28 \end{isamarkuptext}% |
28 \end{isamarkuptext}% |
29 \isamarkuptrue% |
29 \isamarkuptrue% |
30 \isacommand{consts}\isanewline |
30 \isacommand{consts}\isanewline |
31 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
31 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
32 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
32 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
33 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
33 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
34 % |
34 % |
35 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
36 \noindent Next we define class \isa{monoid} of monoids with |
36 \noindent Next we define class \isa{monoid} of monoids with |
37 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
37 operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class |
38 axioms are allowed for user convenience --- they simply represent |
38 axioms are allowed for user convenience --- they simply represent |
39 the conjunction of their respective universal closures.% |
39 the conjunction of their respective universal closures.% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline |
42 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline |
43 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
43 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
44 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
44 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
45 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
45 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
46 % |
46 % |
47 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
48 \noindent So class \isa{monoid} contains exactly those types |
48 \noindent So class \isa{monoid} contains exactly those types |
49 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} |
49 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} |
50 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
50 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
51 \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}} |
51 \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} |
52 operation.% |
52 operation.% |
53 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
54 \isamarkuptrue% |
54 \isamarkuptrue% |
55 % |
55 % |
56 \begin{isamarkuptext}% |
56 \begin{isamarkuptext}% |
63 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
63 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
64 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
64 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
65 \isanewline |
65 \isanewline |
66 \isamarkupfalse% |
66 \isamarkupfalse% |
67 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
67 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
68 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
68 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
69 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
69 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
70 \isanewline |
70 \isanewline |
71 \isamarkupfalse% |
71 \isamarkupfalse% |
72 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
72 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
73 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
73 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
74 % |
74 % |
96 special treatment. Such ``abstract proofs'' usually yield new |
96 special treatment. Such ``abstract proofs'' usually yield new |
97 ``abstract theorems''. For example, we may now derive the following |
97 ``abstract theorems''. For example, we may now derive the following |
98 well-known laws of general groups.% |
98 well-known laws of general groups.% |
99 \end{isamarkuptext}% |
99 \end{isamarkuptext}% |
100 \isamarkuptrue% |
100 \isamarkuptrue% |
101 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
101 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
102 \isamarkupfalse% |
102 \isamarkupfalse% |
103 \isacommand{proof}\ {\isacharminus}\isanewline |
103 \isacommand{proof}\ {\isacharminus}\isanewline |
104 \ \ \isamarkupfalse% |
104 \ \ \isamarkupfalse% |
105 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
105 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
106 \ \ \ \ \isamarkupfalse% |
106 \ \ \ \ \isamarkupfalse% |
107 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
107 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
108 \ \ \isamarkupfalse% |
108 \ \ \isamarkupfalse% |
109 \isacommand{also}\ \isamarkupfalse% |
109 \isacommand{also}\ \isamarkupfalse% |
110 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
110 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
111 \ \ \ \ \isamarkupfalse% |
111 \ \ \ \ \isamarkupfalse% |
112 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
112 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
113 \ \ \isamarkupfalse% |
113 \ \ \isamarkupfalse% |
114 \isacommand{also}\ \isamarkupfalse% |
114 \isacommand{also}\ \isamarkupfalse% |
115 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
115 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
120 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
120 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
121 \ \ \ \ \isamarkupfalse% |
121 \ \ \ \ \isamarkupfalse% |
122 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
122 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
123 \ \ \isamarkupfalse% |
123 \ \ \isamarkupfalse% |
124 \isacommand{also}\ \isamarkupfalse% |
124 \isacommand{also}\ \isamarkupfalse% |
125 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
125 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
126 \ \ \ \ \isamarkupfalse% |
126 \ \ \ \ \isamarkupfalse% |
127 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
127 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
128 \ \ \isamarkupfalse% |
128 \ \ \isamarkupfalse% |
129 \isacommand{also}\ \isamarkupfalse% |
129 \isacommand{also}\ \isamarkupfalse% |
130 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
130 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
131 \ \ \ \ \isamarkupfalse% |
131 \ \ \ \ \isamarkupfalse% |
132 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
132 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
133 \ \ \isamarkupfalse% |
133 \ \ \isamarkupfalse% |
134 \isacommand{also}\ \isamarkupfalse% |
134 \isacommand{also}\ \isamarkupfalse% |
135 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
135 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
136 \ \ \ \ \isamarkupfalse% |
136 \ \ \ \ \isamarkupfalse% |
137 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
137 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
138 \ \ \isamarkupfalse% |
138 \ \ \isamarkupfalse% |
139 \isacommand{also}\ \isamarkupfalse% |
139 \isacommand{also}\ \isamarkupfalse% |
140 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
140 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
141 \ \ \ \ \isamarkupfalse% |
141 \ \ \ \ \isamarkupfalse% |
142 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
142 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
143 \ \ \isamarkupfalse% |
143 \ \ \isamarkupfalse% |
144 \isacommand{finally}\ \isamarkupfalse% |
144 \isacommand{finally}\ \isamarkupfalse% |
145 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
145 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
150 \begin{isamarkuptext}% |
150 \begin{isamarkuptext}% |
151 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
151 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
152 much easier.% |
152 much easier.% |
153 \end{isamarkuptext}% |
153 \end{isamarkuptext}% |
154 \isamarkuptrue% |
154 \isamarkuptrue% |
155 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
155 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
156 \isamarkupfalse% |
156 \isamarkupfalse% |
157 \isacommand{proof}\ {\isacharminus}\isanewline |
157 \isacommand{proof}\ {\isacharminus}\isanewline |
158 \ \ \isamarkupfalse% |
158 \ \ \isamarkupfalse% |
159 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
159 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
160 \ \ \ \ \isamarkupfalse% |
160 \ \ \ \ \isamarkupfalse% |
161 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
161 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
162 \ \ \isamarkupfalse% |
162 \ \ \isamarkupfalse% |
163 \isacommand{also}\ \isamarkupfalse% |
163 \isacommand{also}\ \isamarkupfalse% |
164 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
164 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
165 \ \ \ \ \isamarkupfalse% |
165 \ \ \ \ \isamarkupfalse% |
166 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
166 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
167 \ \ \isamarkupfalse% |
167 \ \ \isamarkupfalse% |
168 \isacommand{also}\ \isamarkupfalse% |
168 \isacommand{also}\ \isamarkupfalse% |
169 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
169 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
170 \ \ \ \ \isamarkupfalse% |
170 \ \ \ \ \isamarkupfalse% |
171 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
171 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
172 \ \ \isamarkupfalse% |
172 \ \ \isamarkupfalse% |
173 \isacommand{also}\ \isamarkupfalse% |
173 \isacommand{also}\ \isamarkupfalse% |
174 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
174 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
249 \ \ \isamarkupfalse% |
249 \ \ \isamarkupfalse% |
250 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
250 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
251 \ \ \ \ \isamarkupfalse% |
251 \ \ \ \ \isamarkupfalse% |
252 \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
252 \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
253 \ \ \isamarkupfalse% |
253 \ \ \isamarkupfalse% |
254 \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
254 \isacommand{show}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
255 \ \ \ \ \isamarkupfalse% |
255 \ \ \ \ \isamarkupfalse% |
256 \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
256 \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
257 \ \ \isamarkupfalse% |
257 \ \ \isamarkupfalse% |
258 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
258 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
259 \ \ \ \ \isamarkupfalse% |
259 \ \ \ \ \isamarkupfalse% |
260 \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
260 \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
261 \isamarkupfalse% |
261 \isamarkupfalse% |
262 \isacommand{qed}\isamarkupfalse% |
262 \isacommand{qed}\isamarkupfalse% |
263 % |
263 % |
287 logical level and then transferred to Isabelle's type signature |
287 logical level and then transferred to Isabelle's type signature |
288 level. |
288 level. |
289 |
289 |
290 \medskip As a typical example, we show that type \isa{bool} with |
290 \medskip As a typical example, we show that type \isa{bool} with |
291 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
291 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
292 \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% |
292 \isa{False} as \isa{{\isasymone}} forms an Abelian group.% |
293 \end{isamarkuptext}% |
293 \end{isamarkuptext}% |
294 \isamarkuptrue% |
294 \isamarkuptrue% |
295 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
295 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
296 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
296 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
297 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
297 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
298 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
298 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
299 % |
299 % |
300 \begin{isamarkuptext}% |
300 \begin{isamarkuptext}% |
301 \medskip It is important to note that above $\DEFS$ are just |
301 \medskip It is important to note that above $\DEFS$ are just |
302 overloaded meta-level constant definitions, where type classes are |
302 overloaded meta-level constant definitions, where type classes are |
303 not yet involved at all. This form of constant definition with |
303 not yet involved at all. This form of constant definition with |
340 this new instance automatically. |
340 this new instance automatically. |
341 |
341 |
342 \medskip We could now also instantiate our group theory classes to |
342 \medskip We could now also instantiate our group theory classes to |
343 many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
343 many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
344 (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
344 (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
345 and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} |
345 and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} |
346 (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
346 (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
347 characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}} |
347 characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}} |
348 really become overloaded, i.e.\ have different meanings on different |
348 really become overloaded, i.e.\ have different meanings on different |
349 types.% |
349 types.% |
350 \end{isamarkuptext}% |
350 \end{isamarkuptext}% |
351 \isamarkuptrue% |
351 \isamarkuptrue% |
352 % |
352 % |