1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Product}% |
3 \def\isabellecontext{Product}% |
4 \isamarkuptrue% |
|
5 % |
4 % |
6 \isamarkupheader{Syntactic classes% |
5 \isamarkupheader{Syntactic classes% |
7 } |
6 } |
|
7 \isamarkuptrue% |
8 % |
8 % |
9 \isadelimtheory |
9 \isadelimtheory |
10 % |
10 % |
11 \endisadelimtheory |
11 \endisadelimtheory |
12 % |
12 % |
13 \isatagtheory |
13 \isatagtheory |
14 \isamarkupfalse% |
14 \isacommand{theory}\isamarkupfalse% |
15 \isacommand{theory}\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}% |
15 \ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}% |
16 \endisatagtheory |
16 \endisatagtheory |
17 {\isafoldtheory}% |
17 {\isafoldtheory}% |
18 % |
18 % |
19 \isadelimtheory |
19 \isadelimtheory |
20 % |
20 % |
21 \endisadelimtheory |
21 \endisadelimtheory |
22 \isamarkuptrue% |
|
23 % |
22 % |
24 \begin{isamarkuptext}% |
23 \begin{isamarkuptext}% |
25 \medskip\noindent There is still a feature of Isabelle's type system |
24 \medskip\noindent There is still a feature of Isabelle's type system |
26 left that we have not yet discussed. When declaring polymorphic |
25 left that we have not yet discussed. When declaring polymorphic |
27 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |
26 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |
32 universal class of HOL, this is not really a constraint at all. |
31 universal class of HOL, this is not really a constraint at all. |
33 |
32 |
34 The \isa{product} class below provides a less degenerate example of |
33 The \isa{product} class below provides a less degenerate example of |
35 syntactic type classes.% |
34 syntactic type classes.% |
36 \end{isamarkuptext}% |
35 \end{isamarkuptext}% |
37 \isamarkupfalse% |
36 \isamarkuptrue% |
38 \isacommand{axclass}\isanewline |
37 \isacommand{axclass}\isamarkupfalse% |
|
38 \isanewline |
39 \ \ product\ {\isasymsubseteq}\ type\isanewline |
39 \ \ product\ {\isasymsubseteq}\ type\isanewline |
40 \isamarkupfalse% |
40 \isacommand{consts}\isamarkupfalse% |
41 \isacommand{consts}\isanewline |
41 \isanewline |
42 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue% |
42 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}% |
43 % |
|
44 \begin{isamarkuptext}% |
43 \begin{isamarkuptext}% |
45 Here class \isa{product} is defined as subclass of \isa{type} |
44 Here class \isa{product} is defined as subclass of \isa{type} |
46 without any additional axioms. This effects in logical equivalence |
45 without any additional axioms. This effects in logical equivalence |
47 of \isa{product} and \isa{type}, as is reflected by the trivial |
46 of \isa{product} and \isa{type}, as is reflected by the trivial |
48 introduction rule generated for this definition. |
47 introduction rule generated for this definition. |
65 constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
64 constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
66 |
65 |
67 This is done for class \isa{product} and type \isa{bool} as |
66 This is done for class \isa{product} and type \isa{bool} as |
68 follows.% |
67 follows.% |
69 \end{isamarkuptext}% |
68 \end{isamarkuptext}% |
70 \isamarkupfalse% |
69 \isamarkuptrue% |
71 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product% |
70 \isacommand{instance}\isamarkupfalse% |
|
71 \ bool\ {\isacharcolon}{\isacharcolon}\ product% |
72 \isadelimproof |
72 \isadelimproof |
73 \ % |
73 \ % |
74 \endisadelimproof |
74 \endisadelimproof |
75 % |
75 % |
76 \isatagproof |
76 \isatagproof |
77 \isamarkupfalse% |
77 \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
78 \isacommand{{\isachardot}{\isachardot}}% |
78 % |
79 \endisatagproof |
79 \endisatagproof |
80 {\isafoldproof}% |
80 {\isafoldproof}% |
81 % |
81 % |
82 \isadelimproof |
82 \isadelimproof |
83 % |
83 % |
84 \endisadelimproof |
84 \endisadelimproof |
85 \isanewline |
85 \isanewline |
86 \isamarkupfalse% |
86 \isacommand{defs}\isamarkupfalse% |
87 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
87 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
88 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkuptrue% |
88 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}% |
89 % |
|
90 \begin{isamarkuptext}% |
89 \begin{isamarkuptext}% |
91 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
90 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
92 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
91 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
93 known to the type checker. |
92 known to the type checker. |
94 |
93 |