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\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline |
23 \ \ inverse\ ::\ {"}'a\ =>\ 'a{"}\ \ \ \ \ \ \ \ ({"}(\_{\isasyminv}){"}\ [1000]\ 999)\isanewline |
23 \ \ inverse\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}1000{\isacharbrackright}\ 999{\isacharparenright}\isanewline |
24 \ \ one\ ::\ 'a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}{\isasymunit}{"})% |
24 \ \ one\ ::\ {\isacharprime}a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}% |
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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
33 \ \ assoc:\ \ \ \ \ \ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
33 \ \ assoc:\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
34 \ \ left\_unit:\ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
34 \ \ left{\isacharunderscore}unit:\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline |
35 \ \ right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}% |
35 \ \ right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}% |
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 the $\TIMES$ operation.% |
40 and right unit element for the $\TIMES$ operation.% |
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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
51 \ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
51 \ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
52 \isanewline |
52 \isanewline |
53 \isacommand{axclass}\isanewline |
53 \isacommand{axclass}\isanewline |
54 \ \ group\ <\ semigroup\isanewline |
54 \ \ group\ {\isacharless}\ semigroup\isanewline |
55 \ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
55 \ \ left{\isacharunderscore}unit:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline |
56 \ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline |
56 \ \ left{\isacharunderscore}inverse:\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{\isachardoublequote}\isanewline |
57 \isanewline |
57 \isanewline |
58 \isacommand{axclass}\isanewline |
58 \isacommand{axclass}\isanewline |
59 \ \ agroup\ <\ group\isanewline |
59 \ \ agroup\ {\isacharless}\ group\isanewline |
60 \ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}% |
60 \ \ commute:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{\isachardoublequote}% |
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{\isacharunderscore}right{\isacharunderscore}inverse:\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
89 \isacommand{proof}\ -\isanewline |
89 \isacommand{proof}\ {\isacharminus}\isanewline |
90 \ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ (x\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline |
90 \ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
91 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
91 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline |
92 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
92 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline |
93 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
93 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline |
94 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
94 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline |
95 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
95 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
96 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x)\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
96 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline |
97 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
97 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline |
98 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
98 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline |
99 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
99 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
100 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ ({\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline |
100 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
101 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
101 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline |
102 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline |
102 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline |
103 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
103 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline |
104 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}{"}\isanewline |
104 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}{\isachardoublequote}\isanewline |
105 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
105 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\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{\isacharunderscore}right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
114 \isacommand{proof}\ -\isanewline |
114 \isacommand{proof}\ {\isacharminus}\isanewline |
115 \ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x){"}\isanewline |
115 \ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
116 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline |
116 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
117 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{"}\isanewline |
117 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline |
118 \ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline |
118 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline |
119 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{"}\isanewline |
119 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline |
120 \ \ \ \ \isacommand{by}\ (simp\ only:\ group\_right\_inverse)\isanewline |
120 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
121 \ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x{"}\isanewline |
121 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x{\isachardoublequote}\isanewline |
122 \ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline |
122 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\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 |
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\ {\isacharless}\ semigroup\isanewline |
173 \isacommand{proof}\ intro\_classes\isanewline |
173 \isacommand{proof}\ intro{\isacharunderscore}classes\isanewline |
174 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}monoid{"}\isanewline |
174 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline |
175 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
175 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
176 \ \ \ \ \isacommand{by}\ (rule\ monoid.assoc)\isanewline |
176 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid.assoc{\isacharparenright}\isanewline |
177 \isacommand{qed}\isanewline |
177 \isacommand{qed}\isanewline |
178 \isanewline |
178 \isanewline |
179 \isacommand{instance}\ group\ <\ monoid\isanewline |
179 \isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline |
180 \isacommand{proof}\ intro\_classes\isanewline |
180 \isacommand{proof}\ intro{\isacharunderscore}classes\isanewline |
181 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}group{"}\isanewline |
181 \ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline |
182 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline |
182 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
183 \ \ \ \ \isacommand{by}\ (rule\ semigroup.assoc)\isanewline |
183 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup.assoc{\isacharparenright}\isanewline |
184 \ \ \isacommand{show}\ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline |
184 \ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline |
185 \ \ \ \ \isacommand{by}\ (rule\ group.left\_unit)\isanewline |
185 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline |
186 \ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}\isanewline |
186 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}\isanewline |
187 \ \ \ \ \isacommand{by}\ (rule\ group\_right\_unit)\isanewline |
187 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\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 |
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 $\TIMES$ operation, 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}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
218 \ \ times\_bool\_def:\ \ \ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ (y{\isasymColon}bool){"}\isanewline |
218 \ \ times{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
219 \ \ inverse\_bool\_def:\ {"}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{"}\isanewline |
219 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
220 \ \ unit\_bool\_def:\ \ \ \ {"}{\isasymunit}\ {\isasymequiv}\ False{"}% |
220 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}% |
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 |
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}\ {\isacharparenleft}intro{\isacharunderscore}classes,\isanewline |
237 \ \ \ \ unfold\ times\_bool\_def\ inverse\_bool\_def\ unit\_bool\_def)\isanewline |
237 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\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}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ =\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
240 \ \ \isacommand{show}\ {"}(False\ {\isasymnoteq}\ x)\ =\ x{"}\ \isacommand{by}\ blast\isanewline |
240 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ =\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
241 \ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ x)\ =\ False{"}\ \isacommand{by}\ blast\isanewline |
241 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ =\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
242 \ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ y)\ =\ (y\ {\isasymnoteq}\ x){"}\ \isacommand{by}\ blast\isanewline |
242 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ =\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \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}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
273 \ \ times\_prod\_def:\ {"}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q){"}% |
273 \ \ times{\isacharunderscore}prod{\isacharunderscore}def:\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}% |
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}\ {\isacharasterisk}\ ::\ {\isacharparenleft}semigroup,\ semigroup{\isacharparenright}\ semigroup\isanewline |
281 \isacommand{proof}\ (intro\_classes,\ unfold\ times\_prod\_def)\isanewline |
281 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
282 \ \ \isacommand{fix}\ p\ q\ r\ ::\ {"}'a{\isasymColon}semigroup\ {\isasymtimes}\ 'b{\isasymColon}semigroup{"}\isanewline |
282 \ \ \isacommand{fix}\ p\ q\ r\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\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 \ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r,\isanewline |
285 \ \ \ \ \ \ snd\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ snd\ r)\ =\isanewline |
285 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ =\isanewline |
286 \ \ \ \ \ \ \ (fst\ p\ {\isasymOtimes}\ fst\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r),\isanewline |
286 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright},\isanewline |
287 \ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r)){"}\isanewline |
287 \ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
288 \ \ \ \ \isacommand{by}\ (simp\ add:\ semigroup.assoc)\isanewline |
288 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add:\ semigroup.assoc{\isacharparenright}\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 |