38 \begin{isamarkuptext}% |
38 \begin{isamarkuptext}% |
39 We specify \emph{semigroups} as subclass of \isa{plus}:% |
39 We specify \emph{semigroups} as subclass of \isa{plus}:% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{class}\isamarkupfalse% |
42 \isacommand{class}\isamarkupfalse% |
43 \ semigroup\ {\isacharequal}\ plus\ {\isacharplus}\isanewline |
43 \ semigroup\ {\isaliteral{3D}{\isacharequal}}\ plus\ {\isaliteral{2B}{\isacharplus}}\isanewline |
44 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}% |
44 \ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
45 \begin{isamarkuptext}% |
45 \begin{isamarkuptext}% |
46 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification requires that |
46 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification requires that |
47 all instances of \isa{semigroup} obey \hyperlink{fact.assoc:}{\mbox{\isa{assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isacharprime}a{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}}. |
47 all instances of \isa{semigroup} obey \hyperlink{fact.assoc:}{\mbox{\isa{assoc{\isaliteral{3A}{\isacharcolon}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. |
48 |
48 |
49 We can use this class axiom to derive further abstract theorems |
49 We can use this class axiom to derive further abstract theorems |
50 relative to class \isa{semigroup}:% |
50 relative to class \isa{semigroup}:% |
51 \end{isamarkuptext}% |
51 \end{isamarkuptext}% |
52 \isamarkuptrue% |
52 \isamarkuptrue% |
53 \isacommand{lemma}\isamarkupfalse% |
53 \isacommand{lemma}\isamarkupfalse% |
54 \ assoc{\isacharunderscore}left{\isacharcolon}\isanewline |
54 \ assoc{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{3A}{\isacharcolon}}\isanewline |
55 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
55 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
56 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline |
56 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
57 % |
57 % |
58 \isadelimproof |
58 \isadelimproof |
59 \ \ % |
59 \ \ % |
60 \endisadelimproof |
60 \endisadelimproof |
61 % |
61 % |
62 \isatagproof |
62 \isatagproof |
63 \isacommand{using}\isamarkupfalse% |
63 \isacommand{using}\isamarkupfalse% |
64 \ assoc\ \isacommand{by}\isamarkupfalse% |
64 \ assoc\ \isacommand{by}\isamarkupfalse% |
65 \ {\isacharparenleft}rule\ sym{\isacharparenright}% |
65 \ {\isaliteral{28}{\isacharparenleft}}rule\ sym{\isaliteral{29}{\isacharparenright}}% |
66 \endisatagproof |
66 \endisatagproof |
67 {\isafoldproof}% |
67 {\isafoldproof}% |
68 % |
68 % |
69 \isadelimproof |
69 \isadelimproof |
70 % |
70 % |
71 \endisadelimproof |
71 \endisadelimproof |
72 % |
72 % |
73 \begin{isamarkuptext}% |
73 \begin{isamarkuptext}% |
74 \noindent The \isa{semigroup} constraint on type \isa{{\isacharprime}a} restricts instantiations of \isa{{\isacharprime}a} to types of class |
74 \noindent The \isa{semigroup} constraint on type \isa{{\isaliteral{27}{\isacharprime}}a} restricts instantiations of \isa{{\isaliteral{27}{\isacharprime}}a} to types of class |
75 \isa{semigroup} and during the proof enables us to use the fact |
75 \isa{semigroup} and during the proof enables us to use the fact |
76 \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class |
76 \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class |
77 \isa{semigroup}. The main advantage of classes is that theorems |
77 \isa{semigroup}. The main advantage of classes is that theorems |
78 can be proved in the abstract and freely reused for each instance. |
78 can be proved in the abstract and freely reused for each instance. |
79 |
79 |
80 On instantiation, we have to give a proof that the given operations |
80 On instantiation, we have to give a proof that the given operations |
81 obey the class axioms:% |
81 obey the class axioms:% |
82 \end{isamarkuptext}% |
82 \end{isamarkuptext}% |
83 \isamarkuptrue% |
83 \isamarkuptrue% |
84 \isacommand{instantiation}\isamarkupfalse% |
84 \isacommand{instantiation}\isamarkupfalse% |
85 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline |
85 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline |
86 \isakeyword{begin}\isanewline |
86 \isakeyword{begin}\isanewline |
87 \isanewline |
87 \isanewline |
88 \isacommand{instance}\isamarkupfalse% |
88 \isacommand{instance}\isamarkupfalse% |
89 % |
89 % |
90 \isadelimproof |
90 \isadelimproof |
94 \isatagproof |
94 \isatagproof |
95 \isacommand{proof}\isamarkupfalse% |
95 \isacommand{proof}\isamarkupfalse% |
96 % |
96 % |
97 \begin{isamarkuptxt}% |
97 \begin{isamarkuptxt}% |
98 \noindent The proof opens with a default proof step, which for |
98 \noindent The proof opens with a default proof step, which for |
99 instance judgements invokes method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}.% |
99 instance judgements invokes method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}.% |
100 \end{isamarkuptxt}% |
100 \end{isamarkuptxt}% |
101 \isamarkuptrue% |
101 \isamarkuptrue% |
102 \ \ \isacommand{fix}\isamarkupfalse% |
102 \ \ \isacommand{fix}\isamarkupfalse% |
103 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
103 \ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
104 \ \ \isacommand{show}\isamarkupfalse% |
104 \ \ \isacommand{show}\isamarkupfalse% |
105 \ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}\ {\isasymoplus}\ q\ {\isacharequal}\ m\ {\isasymoplus}\ {\isacharparenleft}n\ {\isasymoplus}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline |
105 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
106 \ \ \ \ \isacommand{by}\isamarkupfalse% |
106 \ \ \ \ \isacommand{by}\isamarkupfalse% |
107 \ {\isacharparenleft}induct\ m{\isacharparenright}\ simp{\isacharunderscore}all\isanewline |
107 \ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
108 \isacommand{qed}\isamarkupfalse% |
108 \isacommand{qed}\isamarkupfalse% |
109 % |
109 % |
110 \endisatagproof |
110 \endisatagproof |
111 {\isafoldproof}% |
111 {\isafoldproof}% |
112 % |
112 % |
134 % |
134 % |
135 \isatagproof |
135 \isatagproof |
136 \isacommand{proof}\isamarkupfalse% |
136 \isacommand{proof}\isamarkupfalse% |
137 \isanewline |
137 \isanewline |
138 \ \ \isacommand{fix}\isamarkupfalse% |
138 \ \ \isacommand{fix}\isamarkupfalse% |
139 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
139 \ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
140 \ \ \isacommand{show}\isamarkupfalse% |
140 \ \ \isacommand{show}\isamarkupfalse% |
141 \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
141 \ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
142 \ \ \ \ \isacommand{by}\isamarkupfalse% |
142 \ \ \ \ \isacommand{by}\isamarkupfalse% |
143 \ {\isacharparenleft}cases\ p\isactrlisub {\isadigit{1}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{3}}{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}% |
143 \ {\isaliteral{28}{\isacharparenleft}}cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ cases\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}% |
144 \begin{isamarkuptxt}% |
144 \begin{isamarkuptxt}% |
145 \noindent Associativity of product semigroups is established |
145 \noindent Associativity of product semigroups is established |
146 using the hypothetical associativity \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} of the type |
146 using the hypothetical associativity \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} of the type |
147 components, which holds due to the \isa{semigroup} constraints |
147 components, which holds due to the \isa{semigroup} constraints |
148 imposed on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. |
148 imposed on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. |
171 left-hand neutral) by extending \isa{semigroup} with one additional |
171 left-hand neutral) by extending \isa{semigroup} with one additional |
172 parameter \isa{neutral} together with its property:% |
172 parameter \isa{neutral} together with its property:% |
173 \end{isamarkuptext}% |
173 \end{isamarkuptext}% |
174 \isamarkuptrue% |
174 \isamarkuptrue% |
175 \isacommand{class}\isamarkupfalse% |
175 \isacommand{class}\isamarkupfalse% |
176 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
176 \ monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline |
177 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
177 \ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
178 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% |
178 \ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
179 \begin{isamarkuptext}% |
179 \begin{isamarkuptext}% |
180 \noindent Again, we prove some instances, by providing |
180 \noindent Again, we prove some instances, by providing |
181 suitable parameter definitions and proofs for the additional |
181 suitable parameter definitions and proofs for the additional |
182 specifications.% |
182 specifications.% |
183 \end{isamarkuptext}% |
183 \end{isamarkuptext}% |
184 \isamarkuptrue% |
184 \isamarkuptrue% |
185 \isacommand{instantiation}\isamarkupfalse% |
185 \isacommand{instantiation}\isamarkupfalse% |
186 \ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline |
186 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline |
187 \isakeyword{begin}\isanewline |
187 \isakeyword{begin}\isanewline |
188 \isanewline |
188 \isanewline |
189 \isacommand{definition}\isamarkupfalse% |
189 \isacommand{definition}\isamarkupfalse% |
190 \isanewline |
190 \isanewline |
191 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
191 \ \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
192 \isanewline |
192 \isanewline |
193 \isacommand{instance}\isamarkupfalse% |
193 \isacommand{instance}\isamarkupfalse% |
194 % |
194 % |
195 \isadelimproof |
195 \isadelimproof |
196 \ % |
196 \ % |
198 % |
198 % |
199 \isatagproof |
199 \isatagproof |
200 \isacommand{proof}\isamarkupfalse% |
200 \isacommand{proof}\isamarkupfalse% |
201 \isanewline |
201 \isanewline |
202 \ \ \isacommand{fix}\isamarkupfalse% |
202 \ \ \isacommand{fix}\isamarkupfalse% |
203 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
203 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
204 \ \ \isacommand{show}\isamarkupfalse% |
204 \ \ \isacommand{show}\isamarkupfalse% |
205 \ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
205 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
206 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
206 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
207 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
207 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
208 \ simp\isanewline |
208 \ simp\isanewline |
209 \isacommand{qed}\isamarkupfalse% |
209 \isacommand{qed}\isamarkupfalse% |
210 % |
210 % |
211 \endisatagproof |
211 \endisatagproof |
212 {\isafoldproof}% |
212 {\isafoldproof}% |
241 % |
241 % |
242 \isatagproof |
242 \isatagproof |
243 \isacommand{proof}\isamarkupfalse% |
243 \isacommand{proof}\isamarkupfalse% |
244 \isanewline |
244 \isanewline |
245 \ \ \isacommand{fix}\isamarkupfalse% |
245 \ \ \isacommand{fix}\isamarkupfalse% |
246 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline |
246 \ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
247 \ \ \isacommand{show}\isamarkupfalse% |
247 \ \ \isacommand{show}\isamarkupfalse% |
248 \ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline |
248 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
249 \ \ \ \ \isacommand{by}\isamarkupfalse% |
249 \ \ \ \ \isacommand{by}\isamarkupfalse% |
250 \ {\isacharparenleft}cases\ p{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ neutl{\isacharparenright}\isanewline |
250 \ {\isaliteral{28}{\isacharparenleft}}cases\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
251 \isacommand{qed}\isamarkupfalse% |
251 \isacommand{qed}\isamarkupfalse% |
252 % |
252 % |
253 \endisatagproof |
253 \endisatagproof |
254 {\isafoldproof}% |
254 {\isafoldproof}% |
255 % |
255 % |
282 \begin{isamarkuptext}% |
282 \begin{isamarkuptext}% |
283 \noindent To finish our small algebra example, we add a \isa{group} class:% |
283 \noindent To finish our small algebra example, we add a \isa{group} class:% |
284 \end{isamarkuptext}% |
284 \end{isamarkuptext}% |
285 \isamarkuptrue% |
285 \isamarkuptrue% |
286 \isacommand{class}\isamarkupfalse% |
286 \isacommand{class}\isamarkupfalse% |
287 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
287 \ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
288 \ \ \isakeyword{fixes}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymdiv}\ {\isacharunderscore}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{1}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline |
288 \ \ \isakeyword{fixes}\ inv\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{8}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{8}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
289 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}% |
289 \ \ \isakeyword{assumes}\ invl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}% |
290 \begin{isamarkuptext}% |
290 \begin{isamarkuptext}% |
291 \noindent We continue with a further example for abstract |
291 \noindent We continue with a further example for abstract |
292 proofs relative to type classes:% |
292 proofs relative to type classes:% |
293 \end{isamarkuptext}% |
293 \end{isamarkuptext}% |
294 \isamarkuptrue% |
294 \isamarkuptrue% |
295 \isacommand{lemma}\isamarkupfalse% |
295 \isacommand{lemma}\isamarkupfalse% |
296 \ left{\isacharunderscore}cancel{\isacharcolon}\isanewline |
296 \ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}\isanewline |
297 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline |
297 \ \ \isakeyword{fixes}\ x\ y\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
298 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
298 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
299 % |
299 % |
300 \isadelimproof |
300 \isadelimproof |
301 % |
301 % |
302 \endisadelimproof |
302 \endisadelimproof |
303 % |
303 % |
304 \isatagproof |
304 \isatagproof |
305 \isacommand{proof}\isamarkupfalse% |
305 \isacommand{proof}\isamarkupfalse% |
306 \isanewline |
306 \isanewline |
307 \ \ \isacommand{assume}\isamarkupfalse% |
307 \ \ \isacommand{assume}\isamarkupfalse% |
308 \ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline |
308 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
309 \ \ \isacommand{then}\isamarkupfalse% |
309 \ \ \isacommand{then}\isamarkupfalse% |
310 \ \isacommand{have}\isamarkupfalse% |
310 \ \isacommand{have}\isamarkupfalse% |
311 \ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
311 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
312 \ simp\isanewline |
312 \ simp\isanewline |
313 \ \ \isacommand{then}\isamarkupfalse% |
313 \ \ \isacommand{then}\isamarkupfalse% |
314 \ \isacommand{have}\isamarkupfalse% |
314 \ \isacommand{have}\isamarkupfalse% |
315 \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
315 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
316 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline |
316 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline |
317 \ \ \isacommand{then}\isamarkupfalse% |
317 \ \ \isacommand{then}\isamarkupfalse% |
318 \ \isacommand{show}\isamarkupfalse% |
318 \ \isacommand{show}\isamarkupfalse% |
319 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
319 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
320 \ {\isacharparenleft}simp\ add{\isacharcolon}\ invl\ neutl{\isacharparenright}\isanewline |
320 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ invl\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
321 \isacommand{next}\isamarkupfalse% |
321 \isacommand{next}\isamarkupfalse% |
322 \isanewline |
322 \isanewline |
323 \ \ \isacommand{assume}\isamarkupfalse% |
323 \ \ \isacommand{assume}\isamarkupfalse% |
324 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
324 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
325 \ \ \isacommand{then}\isamarkupfalse% |
325 \ \ \isacommand{then}\isamarkupfalse% |
326 \ \isacommand{show}\isamarkupfalse% |
326 \ \isacommand{show}\isamarkupfalse% |
327 \ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
327 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
328 \ simp\isanewline |
328 \ simp\isanewline |
329 \isacommand{qed}\isamarkupfalse% |
329 \isacommand{qed}\isamarkupfalse% |
330 % |
330 % |
331 \endisatagproof |
331 \endisatagproof |
332 {\isafoldproof}% |
332 {\isafoldproof}% |
353 \isanewline |
353 \isanewline |
354 \ \ \isacommand{fix}\isamarkupfalse% |
354 \ \ \isacommand{fix}\isamarkupfalse% |
355 \ x\isanewline |
355 \ x\isanewline |
356 \ \ \isacommand{from}\isamarkupfalse% |
356 \ \ \isacommand{from}\isamarkupfalse% |
357 \ invl\ \isacommand{have}\isamarkupfalse% |
357 \ invl\ \isacommand{have}\isamarkupfalse% |
358 \ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
358 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
359 \isanewline |
359 \isanewline |
360 \ \ \isacommand{then}\isamarkupfalse% |
360 \ \ \isacommand{then}\isamarkupfalse% |
361 \ \isacommand{have}\isamarkupfalse% |
361 \ \isacommand{have}\isamarkupfalse% |
362 \ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ {\isasymzero}{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ x{\isachardoublequoteclose}\isanewline |
362 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6469763E}{\isasymdiv}}\ x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
363 \ \ \ \ \isacommand{by}\isamarkupfalse% |
363 \ \ \ \ \isacommand{by}\isamarkupfalse% |
364 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl\ invl\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
364 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl\ invl\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
365 \ \ \isacommand{then}\isamarkupfalse% |
365 \ \ \isacommand{then}\isamarkupfalse% |
366 \ \isacommand{show}\isamarkupfalse% |
366 \ \isacommand{show}\isamarkupfalse% |
367 \ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isasymzero}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
367 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{5C3C7A65726F3E}{\isasymzero}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
368 \ {\isacharparenleft}simp\ add{\isacharcolon}\ left{\isacharunderscore}cancel{\isacharparenright}\isanewline |
368 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{29}{\isacharparenright}}\isanewline |
369 \isacommand{qed}\isamarkupfalse% |
369 \isacommand{qed}\isamarkupfalse% |
370 % |
370 % |
371 \endisatagproof |
371 \endisatagproof |
372 {\isafoldproof}% |
372 {\isafoldproof}% |
373 % |
373 % |
445 \isamarkuptrue% |
445 \isamarkuptrue% |
446 % |
446 % |
447 \begin{isamarkuptext}% |
447 \begin{isamarkuptext}% |
448 In our algebra example, we have started with a \emph{syntactic |
448 In our algebra example, we have started with a \emph{syntactic |
449 class} \isa{plus} which only specifies operations but no axioms; it |
449 class} \isa{plus} which only specifies operations but no axioms; it |
450 would have been also possible to start immediately with class \isa{semigroup}, specifying the \isa{{\isasymoplus}} operation and associativity at |
450 would have been also possible to start immediately with class \isa{semigroup}, specifying the \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} operation and associativity at |
451 the same time. |
451 the same time. |
452 |
452 |
453 Which approach is more appropriate depends. Usually it is more |
453 Which approach is more appropriate depends. Usually it is more |
454 convenient to introduce operations and axioms in the same class: then |
454 convenient to introduce operations and axioms in the same class: then |
455 the type checker will automatically insert the corresponding class |
455 the type checker will automatically insert the corresponding class |