2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Product}% |
3 \def\isabellecontext{Product}% |
4 % |
4 % |
5 \isamarkupheader{Syntactic classes% |
5 \isamarkupheader{Syntactic classes% |
6 } |
6 } |
7 \isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}% |
7 \isamarkuptrue% |
|
8 \isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
|
9 % |
8 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
9 \medskip\noindent There is still a feature of Isabelle's type system |
11 \medskip\noindent There is still a feature of Isabelle's type system |
10 left that we have not yet discussed. When declaring polymorphic |
12 left that we have not yet discussed. When declaring polymorphic |
11 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |
13 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |
12 may be constrained by type classes (or even general sorts) in an |
14 may be constrained by type classes (or even general sorts) in an |
15 class of HOL, this is not really a constraint at all. |
17 class of HOL, this is not really a constraint at all. |
16 |
18 |
17 The \isa{product} class below provides a less degenerate example of |
19 The \isa{product} class below provides a less degenerate example of |
18 syntactic type classes.% |
20 syntactic type classes.% |
19 \end{isamarkuptext}% |
21 \end{isamarkuptext}% |
|
22 \isamarkuptrue% |
20 \isacommand{axclass}\isanewline |
23 \isacommand{axclass}\isanewline |
21 \ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
24 \ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
|
25 \isamarkupfalse% |
22 \isacommand{consts}\isanewline |
26 \isacommand{consts}\isanewline |
23 \ \ 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}% |
27 \ \ 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}\isamarkupfalse% |
|
28 % |
24 \begin{isamarkuptext}% |
29 \begin{isamarkuptext}% |
25 Here class \isa{product} is defined as subclass of \isa{term} |
30 Here class \isa{product} is defined as subclass of \isa{term} |
26 without any additional axioms. This effects in logical equivalence |
31 without any additional axioms. This effects in logical equivalence |
27 of \isa{product} and \isa{term}, as is reflected by the trivial |
32 of \isa{product} and \isa{term}, as is reflected by the trivial |
28 introduction rule generated for this definition. |
33 introduction rule generated for this definition. |
47 on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
52 on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
48 |
53 |
49 This is done for class \isa{product} and type \isa{bool} as |
54 This is done for class \isa{product} and type \isa{bool} as |
50 follows.% |
55 follows.% |
51 \end{isamarkuptext}% |
56 \end{isamarkuptext}% |
52 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isacommand{{\isachardot}{\isachardot}}\isanewline |
57 \isamarkuptrue% |
|
58 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse% |
|
59 \isacommand{{\isachardot}{\isachardot}}\isanewline |
|
60 \isamarkupfalse% |
53 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
61 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
54 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}% |
62 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkupfalse% |
|
63 % |
55 \begin{isamarkuptext}% |
64 \begin{isamarkuptext}% |
56 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
65 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
57 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
66 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
58 known to the type checker. |
67 known to the type checker. |
59 |
68 |
73 |
82 |
74 This style of \texttt{instance} would not make much sense in |
83 This style of \texttt{instance} would not make much sense in |
75 Isabelle's meta-logic, because there is no internal notion of |
84 Isabelle's meta-logic, because there is no internal notion of |
76 ``providing operations'' or even ``names of functions''.% |
85 ``providing operations'' or even ``names of functions''.% |
77 \end{isamarkuptext}% |
86 \end{isamarkuptext}% |
78 \isacommand{end}\end{isabellebody}% |
87 \isamarkuptrue% |
|
88 \isacommand{end}\isamarkupfalse% |
|
89 \end{isabellebody}% |
79 %%% Local Variables: |
90 %%% Local Variables: |
80 %%% mode: latex |
91 %%% mode: latex |
81 %%% TeX-master: "root" |
92 %%% TeX-master: "root" |
82 %%% End: |
93 %%% End: |