17 \begin{isamarkuptext}% |
17 \begin{isamarkuptext}% |
18 First we declare some polymorphic constants required later for the |
18 First we declare some polymorphic constants required later for the |
19 signature parts of our structures.% |
19 signature parts of our structures.% |
20 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
21 \isacommand{consts}\isanewline |
21 \isacommand{consts}\isanewline |
22 ~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline |
22 \ \ times\ ::\ {"}'a\ =>\ 'a\ =>\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline |
23 ~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline |
23 \ \ inverse\ ::\ {"}'a\ =>\ 'a{"}\ \ \ \ \ \ \ \ ({"}(\_{\isasyminv}){"}\ [1000]\ 999)\isanewline |
24 ~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})% |
24 \ \ one\ ::\ 'a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}{\isasymunit}{"})% |
25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 \noindent Next we define class $monoid$ of monoids with operations |
26 \noindent Next we define class $monoid$ of monoids with operations |
27 $\TIMES$ and $1$. Note that multiple class axioms are allowed for |
27 $\TIMES$ and $1$. Note that multiple class axioms are allowed for |
28 user convenience --- they simply represent the conjunction of their |
28 user convenience --- they simply represent the conjunction of their |
29 respective universal closures.% |
29 respective universal closures.% |
30 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
31 \isacommand{axclass}\isanewline |
31 \isacommand{axclass}\isanewline |
32 ~~monoid~<~{"}term{"}\isanewline |
32 \ \ monoid\ <\ {"}term{"}\isanewline |
33 ~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline |
33 \ \ assoc:\ \ \ \ \ \ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
34 ~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline |
34 \ \ left\_unit:\ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
35 ~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}% |
35 \ \ right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}% |
36 \begin{isamarkuptext}% |
36 \begin{isamarkuptext}% |
37 \noindent So class $monoid$ contains exactly those types $\tau$ where |
37 \noindent So class $monoid$ contains exactly those types $\tau$ where |
38 $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified |
38 $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified |
39 appropriately, such that $\TIMES$ is associative and $1$ is a left |
39 appropriately, such that $\TIMES$ is associative and $1$ is a left |
40 and right unit element for $\TIMES$.% |
40 and right unit element for the $\TIMES$ operation.% |
41 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
42 % |
42 % |
43 \begin{isamarkuptext}% |
43 \begin{isamarkuptext}% |
44 \medskip Independently of $monoid$, we now define a linear hierarchy |
44 \medskip Independently of $monoid$, we now define a linear hierarchy |
45 of semigroups, general groups and Abelian groups. Note that the |
45 of semigroups, general groups and Abelian groups. Note that the |
46 names of class axioms are automatically qualified with each class |
46 names of class axioms are automatically qualified with each class |
47 name, so we may re-use common names such as $assoc$.% |
47 name, so we may re-use common names such as $assoc$.% |
48 \end{isamarkuptext}% |
48 \end{isamarkuptext}% |
49 \isacommand{axclass}\isanewline |
49 \isacommand{axclass}\isanewline |
50 ~~semigroup~<~{"}term{"}\isanewline |
50 \ \ semigroup\ <\ {"}term{"}\isanewline |
51 ~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline |
51 \ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
52 \isanewline |
52 \isanewline |
53 \isacommand{axclass}\isanewline |
53 \isacommand{axclass}\isanewline |
54 ~~group~<~semigroup\isanewline |
54 \ \ group\ <\ semigroup\isanewline |
55 ~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline |
55 \ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
56 ~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline |
56 \ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline |
57 \isanewline |
57 \isanewline |
58 \isacommand{axclass}\isanewline |
58 \isacommand{axclass}\isanewline |
59 ~~agroup~<~group\isanewline |
59 \ \ agroup\ <\ group\isanewline |
60 ~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}% |
60 \ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}% |
61 \begin{isamarkuptext}% |
61 \begin{isamarkuptext}% |
62 \noindent Class $group$ inherits associativity of $\TIMES$ from |
62 \noindent Class $group$ inherits associativity of $\TIMES$ from |
63 $semigroup$ and adds two further group axioms. Similarly, $agroup$ |
63 $semigroup$ and adds two further group axioms. Similarly, $agroup$ |
64 is defined as the subset of $group$ such that for all of its elements |
64 is defined as the subset of $group$ such that for all of its elements |
65 $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even |
65 $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even |
83 ordinary Isabelle theorems, which may be used in proofs without |
83 ordinary Isabelle theorems, which may be used in proofs without |
84 special treatment. Such ``abstract proofs'' usually yield new |
84 special treatment. Such ``abstract proofs'' usually yield new |
85 ``abstract theorems''. For example, we may now derive the following |
85 ``abstract theorems''. For example, we may now derive the following |
86 well-known laws of general groups.% |
86 well-known laws of general groups.% |
87 \end{isamarkuptext}% |
87 \end{isamarkuptext}% |
88 \isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline |
88 \isacommand{theorem}\ group\_right\_inverse:\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ ({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline |
89 \isacommand{proof}~-\isanewline |
89 \isacommand{proof}\ -\isanewline |
90 ~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline |
90 \ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ (x\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline |
91 ~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline |
91 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
92 ~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline |
92 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
93 ~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline |
93 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
94 ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline |
94 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
95 ~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline |
95 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
96 ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline |
96 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x)\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
97 ~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline |
97 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
98 ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline |
98 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
99 ~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline |
99 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
100 ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline |
100 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ ({\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline |
101 ~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline |
101 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
102 ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline |
102 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
103 ~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline |
103 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
104 ~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline |
104 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}{"}\isanewline |
105 ~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline |
105 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
106 ~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline |
106 \ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline |
107 \isacommand{qed}% |
107 \isacommand{qed}% |
108 \begin{isamarkuptext}% |
108 \begin{isamarkuptext}% |
109 \noindent With $group_right_inverse$ already available, |
109 \noindent With $group_right_inverse$ already available, |
110 $group_right_unit$\label{thm:group-right-unit} is now established |
110 $group_right_unit$\label{thm:group-right-unit} is now established |
111 much easier.% |
111 much easier.% |
112 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
113 \isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}group){"}\isanewline |
113 \isacommand{theorem}\ group\_right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ (x{\isasymColon}'a{\isasymColon}group){"}\isanewline |
114 \isacommand{proof}~-\isanewline |
114 \isacommand{proof}\ -\isanewline |
115 ~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline |
115 \ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x){"}\isanewline |
116 ~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline |
116 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
117 ~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline |
117 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{"}\isanewline |
118 ~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline |
118 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
119 ~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline |
119 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{"}\isanewline |
120 ~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline |
120 \ \ \ \ \isacommand{by}\ (simp\ only:\ group\_right\_inverse)\isanewline |
121 ~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline |
121 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x{"}\isanewline |
122 ~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline |
122 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
123 ~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline |
123 \ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline |
124 \isacommand{qed}% |
124 \isacommand{qed}% |
125 \begin{isamarkuptext}% |
125 \begin{isamarkuptext}% |
126 \medskip Abstract theorems may be instantiated to only those types |
126 \medskip Abstract theorems may be instantiated to only those types |
127 $\tau$ where the appropriate class membership $\tau :: c$ is known at |
127 $\tau$ where the appropriate class membership $\tau :: c$ is known at |
128 Isabelle's type signature level. Since we have $agroup \subseteq |
128 Isabelle's type signature level. Since we have $agroup \subseteq |
167 \caption{Monoids and groups: according to definition, and by proof} |
167 \caption{Monoids and groups: according to definition, and by proof} |
168 \label{fig:monoid-group} |
168 \label{fig:monoid-group} |
169 \end{center} |
169 \end{center} |
170 \end{figure}% |
170 \end{figure}% |
171 \end{isamarkuptext}% |
171 \end{isamarkuptext}% |
172 \isacommand{instance}~monoid~<~semigroup\isanewline |
172 \isacommand{instance}\ monoid\ <\ semigroup\isanewline |
173 \isacommand{proof}~intro\_classes\isanewline |
173 \isacommand{proof}\ intro\_classes\isanewline |
174 ~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}monoid{"}\isanewline |
174 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}monoid{"}\isanewline |
175 ~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline |
175 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
176 ~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline |
176 \ \ \ \ \isacommand{by}\ (rule\ monoid.assoc)\isanewline |
177 \isacommand{qed}\isanewline |
177 \isacommand{qed}\isanewline |
178 \isanewline |
178 \isanewline |
179 \isacommand{instance}~group~<~monoid\isanewline |
179 \isacommand{instance}\ group\ <\ monoid\isanewline |
180 \isacommand{proof}~intro\_classes\isanewline |
180 \isacommand{proof}\ intro\_classes\isanewline |
181 ~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}group{"}\isanewline |
181 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}group{"}\isanewline |
182 ~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline |
182 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
183 ~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline |
183 \ \ \ \ \isacommand{by}\ (rule\ semigroup.assoc)\isanewline |
184 ~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline |
184 \ \ \isacommand{show}\ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
185 ~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline |
185 \ \ \ \ \isacommand{by}\ (rule\ group.left\_unit)\isanewline |
186 ~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline |
186 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}\isanewline |
187 ~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline |
187 \ \ \ \ \isacommand{by}\ (rule\ group\_right\_unit)\isanewline |
188 \isacommand{qed}% |
188 \isacommand{qed}% |
189 \begin{isamarkuptext}% |
189 \begin{isamarkuptext}% |
190 \medskip The $\isakeyword{instance}$ command sets up an appropriate |
190 \medskip The $\isakeyword{instance}$ command sets up an appropriate |
191 goal that represents the class inclusion (or type arity, see |
191 goal that represents the class inclusion (or type arity, see |
192 \secref{sec:inst-arity}) to be proven |
192 \secref{sec:inst-arity}) to be proven |
209 is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of |
209 is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of |
210 class membership may be established at the logical level and then |
210 class membership may be established at the logical level and then |
211 transferred to Isabelle's type signature level. |
211 transferred to Isabelle's type signature level. |
212 |
212 |
213 \medskip As a typical example, we show that type $bool$ with |
213 \medskip As a typical example, we show that type $bool$ with |
214 exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and |
214 exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and |
215 $False$ as $1$ forms an Abelian group.% |
215 $False$ as $1$ forms an Abelian group.% |
216 \end{isamarkuptext}% |
216 \end{isamarkuptext}% |
217 \isacommand{defs}~(\isakeyword{overloaded})\isanewline |
217 \isacommand{defs}\ (\isakeyword{overloaded})\isanewline |
218 ~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline |
218 \ \ times\_bool\_def:\ \ \ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ (y{\isasymColon}bool){"}\isanewline |
219 ~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline |
219 \ \ inverse\_bool\_def:\ {"}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{"}\isanewline |
220 ~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}% |
220 \ \ unit\_bool\_def:\ \ \ \ {"}{\isasymunit}\ {\isasymequiv}\ False{"}% |
221 \begin{isamarkuptext}% |
221 \begin{isamarkuptext}% |
222 \medskip It is important to note that above $\DEFS$ are just |
222 \medskip It is important to note that above $\DEFS$ are just |
223 overloaded meta-level constant definitions, where type classes are |
223 overloaded meta-level constant definitions, where type classes are |
224 not yet involved at all. This form of constant definition with |
224 not yet involved at all. This form of constant definition with |
225 overloading (and optional recursion over the syntactic structure of |
225 overloading (and optional recursion over the syntactic structure of |
230 |
230 |
231 \medskip Since we have chosen above $\DEFS$ of the generic group |
231 \medskip Since we have chosen above $\DEFS$ of the generic group |
232 operations on type $bool$ appropriately, the class membership $bool |
232 operations on type $bool$ appropriately, the class membership $bool |
233 :: agroup$ may be now derived as follows.% |
233 :: agroup$ may be now derived as follows.% |
234 \end{isamarkuptext}% |
234 \end{isamarkuptext}% |
235 \isacommand{instance}~bool~::~agroup\isanewline |
235 \isacommand{instance}\ bool\ ::\ agroup\isanewline |
236 \isacommand{proof}~(intro\_classes,\isanewline |
236 \isacommand{proof}\ (intro\_classes,\isanewline |
237 ~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline |
237 \ \ \ \ unfold\ times\_bool\_def\ inverse\_bool\_def\ unit\_bool\_def)\isanewline |
238 ~~\isacommand{fix}~x~y~z\isanewline |
238 \ \ \isacommand{fix}\ x\ y\ z\isanewline |
239 ~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline |
239 \ \ \isacommand{show}\ {"}((x\ {\isasymnoteq}\ y)\ {\isasymnoteq}\ z)\ =\ (x\ {\isasymnoteq}\ (y\ {\isasymnoteq}\ z)){"}\ \isacommand{by}\ blast\isanewline |
240 ~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline |
240 \ \ \isacommand{show}\ {"}(False\ {\isasymnoteq}\ x)\ =\ x{"}\ \isacommand{by}\ blast\isanewline |
241 ~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline |
241 \ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ x)\ =\ False{"}\ \isacommand{by}\ blast\isanewline |
242 ~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline |
242 \ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ y)\ =\ (y\ {\isasymnoteq}\ x){"}\ \isacommand{by}\ blast\isanewline |
243 \isacommand{qed}% |
243 \isacommand{qed}% |
244 \begin{isamarkuptext}% |
244 \begin{isamarkuptext}% |
245 The result of an $\isakeyword{instance}$ statement is both expressed |
245 The result of an $\isakeyword{instance}$ statement is both expressed |
246 as a theorem of Isabelle's meta-logic, and as a type arity of the |
246 as a theorem of Isabelle's meta-logic, and as a type arity of the |
247 type signature. The latter enables type-inference system to take |
247 type signature. The latter enables type-inference system to take |
267 |
267 |
268 This feature enables us to \emph{lift operations}, say to Cartesian |
268 This feature enables us to \emph{lift operations}, say to Cartesian |
269 products, direct sums or function spaces. Subsequently we lift |
269 products, direct sums or function spaces. Subsequently we lift |
270 $\TIMES$ component-wise to binary products $\alpha \times \beta$.% |
270 $\TIMES$ component-wise to binary products $\alpha \times \beta$.% |
271 \end{isamarkuptext}% |
271 \end{isamarkuptext}% |
272 \isacommand{defs}~(\isakeyword{overloaded})\isanewline |
272 \isacommand{defs}\ (\isakeyword{overloaded})\isanewline |
273 ~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}% |
273 \ \ times\_prod\_def:\ {"}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q){"}% |
274 \begin{isamarkuptext}% |
274 \begin{isamarkuptext}% |
275 It is very easy to see that associativity of $\TIMES^\alpha$ and |
275 It is very easy to see that associativity of $\TIMES^\alpha$ and |
276 $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence |
276 $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence |
277 the binary type constructor $\times$ maps semigroups to semigroups. |
277 the binary type constructor $\times$ maps semigroups to semigroups. |
278 This may be established formally as follows.% |
278 This may be established formally as follows.% |
279 \end{isamarkuptext}% |
279 \end{isamarkuptext}% |
280 \isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline |
280 \isacommand{instance}\ *\ ::\ (semigroup,\ semigroup)\ semigroup\isanewline |
281 \isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline |
281 \isacommand{proof}\ (intro\_classes,\ unfold\ times\_prod\_def)\isanewline |
282 ~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline |
282 \ \ \isacommand{fix}\ p\ q\ r\ ::\ {"}'a{\isasymColon}semigroup\ {\isasymtimes}\ 'b{\isasymColon}semigroup{"}\isanewline |
283 ~~\isacommand{show}\isanewline |
283 \ \ \isacommand{show}\isanewline |
284 ~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline |
284 \ \ \ \ {"}(fst\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ fst\ r,\isanewline |
285 ~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline |
285 \ \ \ \ \ \ snd\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ snd\ r)\ =\isanewline |
286 ~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline |
286 \ \ \ \ \ \ \ (fst\ p\ {\isasymOtimes}\ fst\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r),\isanewline |
287 ~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline |
287 \ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r)){"}\isanewline |
288 ~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline |
288 \ \ \ \ \isacommand{by}\ (simp\ add:\ semigroup.assoc)\isanewline |
289 \isacommand{qed}% |
289 \isacommand{qed}% |
290 \begin{isamarkuptext}% |
290 \begin{isamarkuptext}% |
291 Thus, if we view class instances as ``structures'', then overloaded |
291 Thus, if we view class instances as ``structures'', then overloaded |
292 constant definitions with recursion over types indirectly provide |
292 constant definitions with recursion over types indirectly provide |
293 some kind of ``functors'' --- i.e.\ mappings between abstract |
293 some kind of ``functors'' --- i.e.\ mappings between abstract |