38 % |
37 % |
39 \begin{isamarkuptext}% |
38 \begin{isamarkuptext}% |
40 First we declare some polymorphic constants required later for the |
39 First we declare some polymorphic constants required later for the |
41 signature parts of our structures.% |
40 signature parts of our structures.% |
42 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
43 \isamarkupfalse% |
42 \isamarkuptrue% |
44 \isacommand{consts}\isanewline |
43 \isacommand{consts}\isamarkupfalse% |
45 \ \ 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 |
44 \isanewline |
46 \ \ 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 |
45 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
47 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkuptrue% |
46 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
48 % |
47 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}% |
49 \begin{isamarkuptext}% |
48 \begin{isamarkuptext}% |
50 \noindent Next we define class \isa{monoid} of monoids with |
49 \noindent Next we define class \isa{monoid} of monoids with |
51 operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class |
50 operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class |
52 axioms are allowed for user convenience --- they simply represent |
51 axioms are allowed for user convenience --- they simply represent |
53 the conjunction of their respective universal closures.% |
52 the conjunction of their respective universal closures.% |
54 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
55 \isamarkupfalse% |
54 \isamarkuptrue% |
56 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline |
55 \isacommand{axclass}\isamarkupfalse% |
57 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
56 \ monoid\ {\isasymsubseteq}\ type\isanewline |
58 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
57 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
59 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkuptrue% |
58 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
60 % |
59 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% |
61 \begin{isamarkuptext}% |
60 \begin{isamarkuptext}% |
62 \noindent So class \isa{monoid} contains exactly those types |
61 \noindent So class \isa{monoid} contains exactly those types |
63 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} |
62 \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} |
64 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
63 are specified appropriately, such that \isa{{\isasymodot}} is associative and |
65 \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} |
64 \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} |
71 \medskip Independently of \isa{monoid}, we now define a linear |
70 \medskip Independently of \isa{monoid}, we now define a linear |
72 hierarchy of semigroups, general groups and Abelian groups. Note |
71 hierarchy of semigroups, general groups and Abelian groups. Note |
73 that the names of class axioms are automatically qualified with each |
72 that the names of class axioms are automatically qualified with each |
74 class name, so we may re-use common names such as \isa{assoc}.% |
73 class name, so we may re-use common names such as \isa{assoc}.% |
75 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
76 \isamarkupfalse% |
75 \isamarkuptrue% |
77 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
76 \isacommand{axclass}\isamarkupfalse% |
78 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
77 \ semigroup\ {\isasymsubseteq}\ type\isanewline |
79 \isanewline |
78 \ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
80 \isamarkupfalse% |
79 \isanewline |
81 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
80 \isacommand{axclass}\isamarkupfalse% |
82 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
81 \ group\ {\isasymsubseteq}\ semigroup\isanewline |
83 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
82 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
84 \isanewline |
83 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
85 \isamarkupfalse% |
84 \isanewline |
86 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
85 \isacommand{axclass}\isamarkupfalse% |
87 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkuptrue% |
86 \ agroup\ {\isasymsubseteq}\ group\isanewline |
88 % |
87 \ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}% |
89 \begin{isamarkuptext}% |
88 \begin{isamarkuptext}% |
90 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
89 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
91 from \isa{semigroup} and adds two further group axioms. Similarly, |
90 from \isa{semigroup} and adds two further group axioms. Similarly, |
92 \isa{agroup} is defined as the subset of \isa{group} such that |
91 \isa{agroup} is defined as the subset of \isa{group} such that |
93 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
92 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
109 ordinary Isabelle theorems, which may be used in proofs without |
108 ordinary Isabelle theorems, which may be used in proofs without |
110 special treatment. Such ``abstract proofs'' usually yield new |
109 special treatment. Such ``abstract proofs'' usually yield new |
111 ``abstract theorems''. For example, we may now derive the following |
110 ``abstract theorems''. For example, we may now derive the following |
112 well-known laws of general groups.% |
111 well-known laws of general groups.% |
113 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
114 \isamarkupfalse% |
113 \isamarkuptrue% |
115 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
114 \isacommand{theorem}\isamarkupfalse% |
|
115 \ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline |
116 % |
116 % |
117 \isadelimproof |
117 \isadelimproof |
118 % |
118 % |
119 \endisadelimproof |
119 \endisadelimproof |
120 % |
120 % |
121 \isatagproof |
121 \isatagproof |
122 \isamarkupfalse% |
122 \isacommand{proof}\isamarkupfalse% |
123 \isacommand{proof}\ {\isacharminus}\isanewline |
123 \ {\isacharminus}\isanewline |
124 \ \ \isamarkupfalse% |
124 \ \ \isacommand{have}\isamarkupfalse% |
125 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
125 \ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
126 \ \ \ \ \isamarkupfalse% |
126 \ \ \ \ \isacommand{by}\isamarkupfalse% |
127 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
127 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
128 \ \ \isamarkupfalse% |
128 \ \ \isacommand{also}\isamarkupfalse% |
129 \isacommand{also}\ \isamarkupfalse% |
129 \ \isacommand{have}\isamarkupfalse% |
130 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
130 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
131 \ \ \ \ \isamarkupfalse% |
131 \ \ \ \ \isacommand{by}\isamarkupfalse% |
132 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
132 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
133 \ \ \isamarkupfalse% |
133 \ \ \isacommand{also}\isamarkupfalse% |
134 \isacommand{also}\ \isamarkupfalse% |
134 \ \isacommand{have}\isamarkupfalse% |
135 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
135 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
136 \ \ \ \ \isamarkupfalse% |
136 \ \ \ \ \isacommand{by}\isamarkupfalse% |
137 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
137 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
138 \ \ \isamarkupfalse% |
138 \ \ \isacommand{also}\isamarkupfalse% |
139 \isacommand{also}\ \isamarkupfalse% |
139 \ \isacommand{have}\isamarkupfalse% |
140 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
140 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
141 \ \ \ \ \isamarkupfalse% |
141 \ \ \ \ \isacommand{by}\isamarkupfalse% |
142 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
142 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
143 \ \ \isamarkupfalse% |
143 \ \ \isacommand{also}\isamarkupfalse% |
144 \isacommand{also}\ \isamarkupfalse% |
144 \ \isacommand{have}\isamarkupfalse% |
145 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
145 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
146 \ \ \ \ \isamarkupfalse% |
146 \ \ \ \ \isacommand{by}\isamarkupfalse% |
147 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
147 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
148 \ \ \isamarkupfalse% |
148 \ \ \isacommand{also}\isamarkupfalse% |
149 \isacommand{also}\ \isamarkupfalse% |
149 \ \isacommand{have}\isamarkupfalse% |
150 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
150 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
151 \ \ \ \ \isamarkupfalse% |
151 \ \ \ \ \isacommand{by}\isamarkupfalse% |
152 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
152 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
153 \ \ \isamarkupfalse% |
153 \ \ \isacommand{also}\isamarkupfalse% |
154 \isacommand{also}\ \isamarkupfalse% |
154 \ \isacommand{have}\isamarkupfalse% |
155 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
155 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline |
156 \ \ \ \ \isamarkupfalse% |
156 \ \ \ \ \isacommand{by}\isamarkupfalse% |
157 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
157 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
158 \ \ \isamarkupfalse% |
158 \ \ \isacommand{also}\isamarkupfalse% |
159 \isacommand{also}\ \isamarkupfalse% |
159 \ \isacommand{have}\isamarkupfalse% |
160 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
160 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
161 \ \ \ \ \isamarkupfalse% |
161 \ \ \ \ \isacommand{by}\isamarkupfalse% |
162 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
162 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
163 \ \ \isamarkupfalse% |
163 \ \ \isacommand{finally}\isamarkupfalse% |
164 \isacommand{finally}\ \isamarkupfalse% |
164 \ \isacommand{show}\isamarkupfalse% |
165 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
165 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% |
166 \isacommand{{\isachardot}}\isanewline |
166 \isanewline |
167 \isamarkupfalse% |
167 \isacommand{qed}\isamarkupfalse% |
168 \isacommand{qed}% |
168 % |
169 \endisatagproof |
169 \endisatagproof |
170 {\isafoldproof}% |
170 {\isafoldproof}% |
171 % |
171 % |
172 \isadelimproof |
172 \isadelimproof |
173 % |
173 % |
174 \endisadelimproof |
174 \endisadelimproof |
175 \isamarkuptrue% |
|
176 % |
175 % |
177 \begin{isamarkuptext}% |
176 \begin{isamarkuptext}% |
178 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
177 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
179 much easier.% |
178 much easier.% |
180 \end{isamarkuptext}% |
179 \end{isamarkuptext}% |
181 \isamarkupfalse% |
180 \isamarkuptrue% |
182 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
181 \isacommand{theorem}\isamarkupfalse% |
|
182 \ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline |
183 % |
183 % |
184 \isadelimproof |
184 \isadelimproof |
185 % |
185 % |
186 \endisadelimproof |
186 \endisadelimproof |
187 % |
187 % |
188 \isatagproof |
188 \isatagproof |
189 \isamarkupfalse% |
189 \isacommand{proof}\isamarkupfalse% |
190 \isacommand{proof}\ {\isacharminus}\isanewline |
190 \ {\isacharminus}\isanewline |
191 \ \ \isamarkupfalse% |
191 \ \ \isacommand{have}\isamarkupfalse% |
192 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
192 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline |
193 \ \ \ \ \isamarkupfalse% |
193 \ \ \ \ \isacommand{by}\isamarkupfalse% |
194 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
194 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
195 \ \ \isamarkupfalse% |
195 \ \ \isacommand{also}\isamarkupfalse% |
196 \isacommand{also}\ \isamarkupfalse% |
196 \ \isacommand{have}\isamarkupfalse% |
197 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
197 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline |
198 \ \ \ \ \isamarkupfalse% |
198 \ \ \ \ \isacommand{by}\isamarkupfalse% |
199 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
199 \ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
200 \ \ \isamarkupfalse% |
200 \ \ \isacommand{also}\isamarkupfalse% |
201 \isacommand{also}\ \isamarkupfalse% |
201 \ \isacommand{have}\isamarkupfalse% |
202 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
202 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline |
203 \ \ \ \ \isamarkupfalse% |
203 \ \ \ \ \isacommand{by}\isamarkupfalse% |
204 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
204 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
205 \ \ \isamarkupfalse% |
205 \ \ \isacommand{also}\isamarkupfalse% |
206 \isacommand{also}\ \isamarkupfalse% |
206 \ \isacommand{have}\isamarkupfalse% |
207 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
207 \ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
208 \ \ \ \ \isamarkupfalse% |
208 \ \ \ \ \isacommand{by}\isamarkupfalse% |
209 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
209 \ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
210 \ \ \isamarkupfalse% |
210 \ \ \isacommand{finally}\isamarkupfalse% |
211 \isacommand{finally}\ \isamarkupfalse% |
211 \ \isacommand{show}\isamarkupfalse% |
212 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
212 \ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% |
213 \isacommand{{\isachardot}}\isanewline |
213 \isanewline |
214 \isamarkupfalse% |
214 \isacommand{qed}\isamarkupfalse% |
215 \isacommand{qed}% |
215 % |
216 \endisatagproof |
216 \endisatagproof |
217 {\isafoldproof}% |
217 {\isafoldproof}% |
218 % |
218 % |
219 \isadelimproof |
219 \isadelimproof |
220 % |
220 % |
221 \endisadelimproof |
221 \endisadelimproof |
222 \isamarkuptrue% |
|
223 % |
222 % |
224 \begin{isamarkuptext}% |
223 \begin{isamarkuptext}% |
225 \medskip Abstract theorems may be instantiated to only those types |
224 \medskip Abstract theorems may be instantiated to only those types |
226 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
225 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
227 known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.% |
226 known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.% |
265 \caption{Monoids and groups: according to definition, and by proof} |
264 \caption{Monoids and groups: according to definition, and by proof} |
266 \label{fig:monoid-group} |
265 \label{fig:monoid-group} |
267 \end{center} |
266 \end{center} |
268 \end{figure}% |
267 \end{figure}% |
269 \end{isamarkuptext}% |
268 \end{isamarkuptext}% |
270 \isamarkupfalse% |
269 \isamarkuptrue% |
271 \isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
270 \isacommand{instance}\isamarkupfalse% |
|
271 \ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
272 % |
272 % |
273 \isadelimproof |
273 \isadelimproof |
274 % |
274 % |
275 \endisadelimproof |
275 \endisadelimproof |
276 % |
276 % |
277 \isatagproof |
277 \isatagproof |
278 \isamarkupfalse% |
278 \isacommand{proof}\isamarkupfalse% |
279 \isacommand{proof}\isanewline |
279 \isanewline |
280 \ \ \isamarkupfalse% |
280 \ \ \isacommand{fix}\isamarkupfalse% |
281 \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline |
281 \ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline |
282 \ \ \isamarkupfalse% |
282 \ \ \isacommand{show}\isamarkupfalse% |
283 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
283 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
284 \ \ \ \ \isamarkupfalse% |
284 \ \ \ \ \isacommand{by}\isamarkupfalse% |
285 \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline |
285 \ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline |
286 \isamarkupfalse% |
286 \isacommand{qed}\isamarkupfalse% |
287 \isacommand{qed}% |
287 % |
288 \endisatagproof |
288 \endisatagproof |
289 {\isafoldproof}% |
289 {\isafoldproof}% |
290 % |
290 % |
291 \isadelimproof |
291 \isadelimproof |
292 \isanewline |
292 \isanewline |
293 % |
293 % |
294 \endisadelimproof |
294 \endisadelimproof |
295 \isanewline |
295 \isanewline |
296 \isamarkupfalse% |
296 \isacommand{instance}\isamarkupfalse% |
297 \isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline |
297 \ group\ {\isasymsubseteq}\ monoid\isanewline |
298 % |
298 % |
299 \isadelimproof |
299 \isadelimproof |
300 % |
300 % |
301 \endisadelimproof |
301 \endisadelimproof |
302 % |
302 % |
303 \isatagproof |
303 \isatagproof |
304 \isamarkupfalse% |
304 \isacommand{proof}\isamarkupfalse% |
305 \isacommand{proof}\isanewline |
305 \isanewline |
306 \ \ \isamarkupfalse% |
306 \ \ \isacommand{fix}\isamarkupfalse% |
307 \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline |
307 \ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline |
308 \ \ \isamarkupfalse% |
308 \ \ \isacommand{show}\isamarkupfalse% |
309 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
309 \ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline |
310 \ \ \ \ \isamarkupfalse% |
310 \ \ \ \ \isacommand{by}\isamarkupfalse% |
311 \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
311 \ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
312 \ \ \isamarkupfalse% |
312 \ \ \isacommand{show}\isamarkupfalse% |
313 \isacommand{show}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
313 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
314 \ \ \ \ \isamarkupfalse% |
314 \ \ \ \ \isacommand{by}\isamarkupfalse% |
315 \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
315 \ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
316 \ \ \isamarkupfalse% |
316 \ \ \isacommand{show}\isamarkupfalse% |
317 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
317 \ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
318 \ \ \ \ \isamarkupfalse% |
318 \ \ \ \ \isacommand{by}\isamarkupfalse% |
319 \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
319 \ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
320 \isamarkupfalse% |
320 \isacommand{qed}\isamarkupfalse% |
321 \isacommand{qed}% |
321 % |
322 \endisatagproof |
322 \endisatagproof |
323 {\isafoldproof}% |
323 {\isafoldproof}% |
324 % |
324 % |
325 \isadelimproof |
325 \isadelimproof |
326 % |
326 % |
327 \endisadelimproof |
327 \endisadelimproof |
328 \isamarkuptrue% |
|
329 % |
328 % |
330 \begin{isamarkuptext}% |
329 \begin{isamarkuptext}% |
331 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
330 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
332 represents the class inclusion (or type arity, see |
331 represents the class inclusion (or type arity, see |
333 \secref{sec:inst-arity}) to be proven (see also |
332 \secref{sec:inst-arity}) to be proven (see also |
375 |
374 |
376 \medskip Since we have chosen above $\DEFS$ of the generic group |
375 \medskip Since we have chosen above $\DEFS$ of the generic group |
377 operations on type \isa{bool} appropriately, the class membership |
376 operations on type \isa{bool} appropriately, the class membership |
378 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
377 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
379 \end{isamarkuptext}% |
378 \end{isamarkuptext}% |
380 \isamarkupfalse% |
379 \isamarkuptrue% |
381 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
380 \isacommand{instance}\isamarkupfalse% |
|
381 \ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
382 % |
382 % |
383 \isadelimproof |
383 \isadelimproof |
384 % |
384 % |
385 \endisadelimproof |
385 \endisadelimproof |
386 % |
386 % |
387 \isatagproof |
387 \isatagproof |
388 \isamarkupfalse% |
388 \isacommand{proof}\isamarkupfalse% |
389 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
389 \ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
390 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
390 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
391 \ \ \isamarkupfalse% |
391 \ \ \isacommand{fix}\isamarkupfalse% |
392 \isacommand{fix}\ x\ y\ z\isanewline |
392 \ x\ y\ z\isanewline |
393 \ \ \isamarkupfalse% |
393 \ \ \isacommand{show}\isamarkupfalse% |
394 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
394 \ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
395 \isacommand{by}\ blast\isanewline |
395 \ blast\isanewline |
396 \ \ \isamarkupfalse% |
396 \ \ \isacommand{show}\isamarkupfalse% |
397 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isamarkupfalse% |
397 \ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
398 \isacommand{by}\ blast\isanewline |
398 \ blast\isanewline |
399 \ \ \isamarkupfalse% |
399 \ \ \isacommand{show}\isamarkupfalse% |
400 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isamarkupfalse% |
400 \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
401 \isacommand{by}\ blast\isanewline |
401 \ blast\isanewline |
402 \ \ \isamarkupfalse% |
402 \ \ \isacommand{show}\isamarkupfalse% |
403 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
403 \ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
404 \isacommand{by}\ blast\isanewline |
404 \ blast\isanewline |
405 \isamarkupfalse% |
405 \isacommand{qed}\isamarkupfalse% |
406 \isacommand{qed}% |
406 % |
407 \endisatagproof |
407 \endisatagproof |
408 {\isafoldproof}% |
408 {\isafoldproof}% |
409 % |
409 % |
410 \isadelimproof |
410 \isadelimproof |
411 % |
411 % |
412 \endisadelimproof |
412 \endisadelimproof |
413 \isamarkuptrue% |
|
414 % |
413 % |
415 \begin{isamarkuptext}% |
414 \begin{isamarkuptext}% |
416 The result of an $\INSTANCE$ statement is both expressed as a |
415 The result of an $\INSTANCE$ statement is both expressed as a |
417 theorem of Isabelle's meta-logic, and as a type arity of the type |
416 theorem of Isabelle's meta-logic, and as a type arity of the type |
418 signature. The latter enables type-inference system to take care of |
417 signature. The latter enables type-inference system to take care of |
442 |
441 |
443 This feature enables us to \emph{lift operations}, say to Cartesian |
442 This feature enables us to \emph{lift operations}, say to Cartesian |
444 products, direct sums or function spaces. Subsequently we lift |
443 products, direct sums or function spaces. Subsequently we lift |
445 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
444 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
446 \end{isamarkuptext}% |
445 \end{isamarkuptext}% |
447 \isamarkupfalse% |
446 \isamarkuptrue% |
448 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
447 \isacommand{defs}\isamarkupfalse% |
449 \ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
448 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
450 % |
449 \ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequoteclose}% |
451 \begin{isamarkuptext}% |
450 \begin{isamarkuptext}% |
452 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
451 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
453 and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups |
452 and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups |
454 to semigroups. This may be established formally as follows.% |
453 to semigroups. This may be established formally as follows.% |
455 \end{isamarkuptext}% |
454 \end{isamarkuptext}% |
456 \isamarkupfalse% |
455 \isamarkuptrue% |
457 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
456 \isacommand{instance}\isamarkupfalse% |
|
457 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
458 % |
458 % |
459 \isadelimproof |
459 \isadelimproof |
460 % |
460 % |
461 \endisadelimproof |
461 \endisadelimproof |
462 % |
462 % |
463 \isatagproof |
463 \isatagproof |
464 \isamarkupfalse% |
464 \isacommand{proof}\isamarkupfalse% |
465 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
465 \ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
466 \ \ \isamarkupfalse% |
466 \ \ \isacommand{fix}\isamarkupfalse% |
467 \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline |
467 \ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
468 \ \ \isamarkupfalse% |
468 \ \ \isacommand{show}\isamarkupfalse% |
469 \isacommand{show}\isanewline |
469 \isanewline |
470 \ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
470 \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
471 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
471 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
472 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
472 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
473 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
473 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
474 \ \ \ \ \isamarkupfalse% |
474 \ \ \ \ \isacommand{by}\isamarkupfalse% |
475 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
475 \ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
476 \isamarkupfalse% |
476 \isacommand{qed}\isamarkupfalse% |
477 \isacommand{qed}% |
477 % |
478 \endisatagproof |
478 \endisatagproof |
479 {\isafoldproof}% |
479 {\isafoldproof}% |
480 % |
480 % |
481 \isadelimproof |
481 \isadelimproof |
482 % |
482 % |
483 \endisadelimproof |
483 \endisadelimproof |
484 \isamarkuptrue% |
|
485 % |
484 % |
486 \begin{isamarkuptext}% |
485 \begin{isamarkuptext}% |
487 Thus, if we view class instances as ``structures'', then overloaded |
486 Thus, if we view class instances as ``structures'', then overloaded |
488 constant definitions with recursion over types indirectly provide |
487 constant definitions with recursion over types indirectly provide |
489 some kind of ``functors'' --- i.e.\ mappings between abstract |
488 some kind of ``functors'' --- i.e.\ mappings between abstract |
490 theories.% |
489 theories.% |
491 \end{isamarkuptext}% |
490 \end{isamarkuptext}% |
|
491 \isamarkuptrue% |
492 % |
492 % |
493 \isadelimtheory |
493 \isadelimtheory |
494 % |
494 % |
495 \endisadelimtheory |
495 \endisadelimtheory |
496 % |
496 % |
497 \isatagtheory |
497 \isatagtheory |
498 \isamarkupfalse% |
498 \isacommand{end}\isamarkupfalse% |
499 \isacommand{end}% |
499 % |
500 \endisatagtheory |
500 \endisatagtheory |
501 {\isafoldtheory}% |
501 {\isafoldtheory}% |
502 % |
502 % |
503 \isadelimtheory |
503 \isadelimtheory |
504 % |
504 % |