19 First we declare some polymorphic constants required later for the |
19 First we declare some polymorphic constants required later for the |
20 signature parts of our structures. |
20 signature parts of our structures. |
21 *} |
21 *} |
22 |
22 |
23 consts |
23 consts |
24 times :: "'a => 'a => 'a" (infixl "\<Otimes>" 70) |
24 times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
25 inverse :: "'a => 'a" ("(_\<inv>)" [1000] 999) |
25 inverse :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) |
26 one :: 'a ("\<unit>") |
26 one :: 'a ("\<unit>") |
27 |
27 |
28 text {* |
28 text {* |
29 \noindent Next we define class $monoid$ of monoids with operations |
29 \noindent Next we define class @{text monoid} of monoids with |
30 $\TIMES$ and $1$. Note that multiple class axioms are allowed for |
30 operations @{text \<odot>} and @{text \<unit>}. Note that multiple class |
31 user convenience --- they simply represent the conjunction of their |
31 axioms are allowed for user convenience --- they simply represent the |
32 respective universal closures. |
32 conjunction of their respective universal closures. |
33 *} |
33 *} |
34 |
34 |
35 axclass |
35 axclass monoid < "term" |
36 monoid < "term" |
36 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
37 assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)" |
37 left_unit: "\<unit> \<odot> x = x" |
38 left_unit: "\<unit> \<Otimes> x = x" |
38 right_unit: "x \<odot> \<unit> = x" |
39 right_unit: "x \<Otimes> \<unit> = x" |
39 |
40 |
40 text {* |
41 text {* |
41 \noindent So class @{text monoid} contains exactly those types @{text |
42 \noindent So class $monoid$ contains exactly those types $\tau$ where |
42 \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"} are |
43 $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified |
43 specified appropriately, such that @{text \<odot>} is associative and |
44 appropriately, such that $\TIMES$ is associative and $1$ is a left |
44 @{text \<unit>} is a left and right unit element for the @{text \<odot>} |
45 and right unit element for the $\TIMES$ operation. |
45 operation. |
46 *} |
46 *} |
47 |
47 |
48 text {* |
48 text {* |
49 \medskip Independently of $monoid$, we now define a linear hierarchy |
49 \medskip Independently of @{text monoid}, we now define a linear |
50 of semigroups, general groups and Abelian groups. Note that the |
50 hierarchy of semigroups, general groups and Abelian groups. Note |
51 names of class axioms are automatically qualified with each class |
51 that the names of class axioms are automatically qualified with each |
52 name, so we may re-use common names such as $assoc$. |
52 class name, so we may re-use common names such as @{text assoc}. |
53 *} |
53 *} |
54 |
54 |
55 axclass |
55 axclass semigroup < "term" |
56 semigroup < "term" |
56 assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
57 assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)" |
57 |
58 |
58 axclass group < semigroup |
59 axclass |
59 left_unit: "\<unit> \<odot> x = x" |
60 group < semigroup |
60 left_inverse: "x\<inv> \<odot> x = \<unit>" |
61 left_unit: "\<unit> \<Otimes> x = x" |
61 |
62 left_inverse: "x\<inv> \<Otimes> x = \<unit>" |
62 axclass agroup < group |
63 |
63 commute: "x \<odot> y = y \<odot> x" |
64 axclass |
64 |
65 agroup < group |
65 text {* |
66 commute: "x \<Otimes> y = y \<Otimes> x" |
66 \noindent Class @{text group} inherits associativity of @{text \<odot>} |
67 |
67 from @{text semigroup} and adds two further group axioms. Similarly, |
68 text {* |
68 @{text agroup} is defined as the subset of @{text group} such that |
69 \noindent Class $group$ inherits associativity of $\TIMES$ from |
69 for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} |
70 $semigroup$ and adds two further group axioms. Similarly, $agroup$ |
70 is even commutative. |
71 is defined as the subset of $group$ such that for all of its elements |
|
72 $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even |
|
73 commutative. |
|
74 *} |
71 *} |
75 |
72 |
76 |
73 |
77 subsection {* Abstract reasoning *} |
74 subsection {* Abstract reasoning *} |
78 |
75 |
79 text {* |
76 text {* |
80 In a sense, axiomatic type classes may be viewed as \emph{abstract |
77 In a sense, axiomatic type classes may be viewed as \emph{abstract |
81 theories}. Above class definitions gives rise to abstract axioms |
78 theories}. Above class definitions gives rise to abstract axioms |
82 $assoc$, $left_unit$, $left_inverse$, $commute$, where any of these |
79 @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text |
83 contain a type variable $\alpha :: c$ that is restricted to types of |
80 commute}, where any of these contain a type variable @{text "'a \<Colon> c"} |
84 the corresponding class $c$. \emph{Sort constraints} like this |
81 that is restricted to types of the corresponding class @{text c}. |
85 express a logical precondition for the whole formula. For example, |
82 \emph{Sort constraints} like this express a logical precondition for |
86 $assoc$ states that for all $\tau$, provided that $\tau :: |
83 the whole formula. For example, @{text assoc} states that for all |
87 semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is |
84 @{text \<tau>}, provided that @{text "\<tau> \<Colon> semigroup"}, the operation |
88 associative. |
85 @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative. |
89 |
86 |
90 \medskip From a technical point of view, abstract axioms are just |
87 \medskip From a technical point of view, abstract axioms are just |
91 ordinary Isabelle theorems, which may be used in proofs without |
88 ordinary Isabelle theorems, which may be used in proofs without |
92 special treatment. Such ``abstract proofs'' usually yield new |
89 special treatment. Such ``abstract proofs'' usually yield new |
93 ``abstract theorems''. For example, we may now derive the following |
90 ``abstract theorems''. For example, we may now derive the following |
94 well-known laws of general groups. |
91 well-known laws of general groups. |
95 *} |
92 *} |
96 |
93 |
97 theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>\\<Colon>'a\\<Colon>group)" |
94 theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)" |
98 proof - |
95 proof - |
99 have "x \<Otimes> x\<inv> = \<unit> \<Otimes> (x \<Otimes> x\<inv>)" |
96 have "x \<odot> x\<inv> = \<unit> \<odot> (x \<odot> x\<inv>)" |
100 by (simp only: group.left_unit) |
97 by (simp only: group.left_unit) |
101 also have "... = \<unit> \<Otimes> x \<Otimes> x\<inv>" |
98 also have "... = \<unit> \<odot> x \<odot> x\<inv>" |
102 by (simp only: semigroup.assoc) |
99 by (simp only: semigroup.assoc) |
103 also have "... = (x\<inv>)\<inv> \<Otimes> x\<inv> \<Otimes> x \<Otimes> x\<inv>" |
100 also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>" |
104 by (simp only: group.left_inverse) |
101 by (simp only: group.left_inverse) |
105 also have "... = (x\<inv>)\<inv> \<Otimes> (x\<inv> \<Otimes> x) \<Otimes> x\<inv>" |
102 also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>" |
106 by (simp only: semigroup.assoc) |
103 by (simp only: semigroup.assoc) |
107 also have "... = (x\<inv>)\<inv> \<Otimes> \<unit> \<Otimes> x\<inv>" |
104 also have "... = (x\<inv>)\<inv> \<odot> \<unit> \<odot> x\<inv>" |
108 by (simp only: group.left_inverse) |
105 by (simp only: group.left_inverse) |
109 also have "... = (x\<inv>)\<inv> \<Otimes> (\<unit> \<Otimes> x\<inv>)" |
106 also have "... = (x\<inv>)\<inv> \<odot> (\<unit> \<odot> x\<inv>)" |
110 by (simp only: semigroup.assoc) |
107 by (simp only: semigroup.assoc) |
111 also have "... = (x\<inv>)\<inv> \<Otimes> x\<inv>" |
108 also have "... = (x\<inv>)\<inv> \<odot> x\<inv>" |
112 by (simp only: group.left_unit) |
109 by (simp only: group.left_unit) |
113 also have "... = \<unit>" |
110 also have "... = \<unit>" |
114 by (simp only: group.left_inverse) |
111 by (simp only: group.left_inverse) |
115 finally show ?thesis . |
112 finally show ?thesis . |
116 qed |
113 qed |
117 |
114 |
118 text {* |
115 text {* |
119 \noindent With $group_right_inverse$ already available, |
116 \noindent With @{text group_right_inverse} already available, @{text |
120 $group_right_unit$\label{thm:group-right-unit} is now established |
117 group_right_unit}\label{thm:group-right-unit} is now established much |
121 much easier. |
118 easier. |
122 *} |
119 *} |
123 |
120 |
124 theorem group_right_unit: "x \<Otimes> \<unit> = (x\\<Colon>'a\\<Colon>group)" |
121 theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)" |
125 proof - |
122 proof - |
126 have "x \<Otimes> \<unit> = x \<Otimes> (x\<inv> \<Otimes> x)" |
123 have "x \<odot> \<unit> = x \<odot> (x\<inv> \<odot> x)" |
127 by (simp only: group.left_inverse) |
124 by (simp only: group.left_inverse) |
128 also have "... = x \<Otimes> x\<inv> \<Otimes> x" |
125 also have "... = x \<odot> x\<inv> \<odot> x" |
129 by (simp only: semigroup.assoc) |
126 by (simp only: semigroup.assoc) |
130 also have "... = \<unit> \<Otimes> x" |
127 also have "... = \<unit> \<odot> x" |
131 by (simp only: group_right_inverse) |
128 by (simp only: group_right_inverse) |
132 also have "... = x" |
129 also have "... = x" |
133 by (simp only: group.left_unit) |
130 by (simp only: group.left_unit) |
134 finally show ?thesis . |
131 finally show ?thesis . |
135 qed |
132 qed |
136 |
133 |
137 text {* |
134 text {* |
138 \medskip Abstract theorems may be instantiated to only those types |
135 \medskip Abstract theorems may be instantiated to only those types |
139 $\tau$ where the appropriate class membership $\tau :: c$ is known at |
136 @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is |
140 Isabelle's type signature level. Since we have $agroup \subseteq |
137 known at Isabelle's type signature level. Since we have @{text |
141 group \subseteq semigroup$ by definition, all theorems of $semigroup$ |
138 "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text |
142 and $group$ are automatically inherited by $group$ and $agroup$. |
139 semigroup} and @{text group} are automatically inherited by @{text |
|
140 group} and @{text agroup}. |
143 *} |
141 *} |
144 |
142 |
145 |
143 |
146 subsection {* Abstract instantiation *} |
144 subsection {* Abstract instantiation *} |
147 |
145 |
148 text {* |
146 text {* |
149 From the definition, the $monoid$ and $group$ classes have been |
147 From the definition, the @{text monoid} and @{text group} classes |
150 independent. Note that for monoids, $right_unit$ had to be included |
148 have been independent. Note that for monoids, @{text right_unit} had |
151 as an axiom, but for groups both $right_unit$ and $right_inverse$ are |
149 to be included as an axiom, but for groups both @{text right_unit} |
152 derivable from the other axioms. With $group_right_unit$ derived as |
150 and @{text right_inverse} are derivable from the other axioms. With |
153 a theorem of group theory (see page~\pageref{thm:group-right-unit}), |
151 @{text group_right_unit} derived as a theorem of group theory (see |
154 we may now instantiate $monoid \subseteq semigroup$ and $group |
152 page~\pageref{thm:group-right-unit}), we may now instantiate @{text |
155 \subseteq monoid$ properly as follows |
153 "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> monoid"} properly as |
156 (cf.\ \figref{fig:monoid-group}). |
154 follows (cf.\ \figref{fig:monoid-group}). |
157 |
155 |
158 \begin{figure}[htbp] |
156 \begin{figure}[htbp] |
159 \begin{center} |
157 \begin{center} |
160 \small |
158 \small |
161 \unitlength 0.6mm |
159 \unitlength 0.6mm |
162 \begin{picture}(65,90)(0,-10) |
160 \begin{picture}(65,90)(0,-10) |
163 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
161 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
164 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
162 \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
165 \put(15,5){\makebox(0,0){$agroup$}} |
163 \put(15,5){\makebox(0,0){@{text agroup}}} |
166 \put(15,25){\makebox(0,0){$group$}} |
164 \put(15,25){\makebox(0,0){@{text group}}} |
167 \put(15,45){\makebox(0,0){$semigroup$}} |
165 \put(15,45){\makebox(0,0){@{text semigroup}}} |
168 \put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}} |
166 \put(30,65){\makebox(0,0){@{text "term"}}} \put(50,45){\makebox(0,0){@{text monoid}}} |
169 \end{picture} |
167 \end{picture} |
170 \hspace{4em} |
168 \hspace{4em} |
171 \begin{picture}(30,90)(0,0) |
169 \begin{picture}(30,90)(0,0) |
172 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
170 \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
173 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
171 \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
174 \put(15,5){\makebox(0,0){$agroup$}} |
172 \put(15,5){\makebox(0,0){@{text agroup}}} |
175 \put(15,25){\makebox(0,0){$group$}} |
173 \put(15,25){\makebox(0,0){@{text group}}} |
176 \put(15,45){\makebox(0,0){$monoid$}} |
174 \put(15,45){\makebox(0,0){@{text monoid}}} |
177 \put(15,65){\makebox(0,0){$semigroup$}} |
175 \put(15,65){\makebox(0,0){@{text semigroup}}} |
178 \put(15,85){\makebox(0,0){$term$}} |
176 \put(15,85){\makebox(0,0){@{text term}}} |
179 \end{picture} |
177 \end{picture} |
180 \caption{Monoids and groups: according to definition, and by proof} |
178 \caption{Monoids and groups: according to definition, and by proof} |
181 \label{fig:monoid-group} |
179 \label{fig:monoid-group} |
182 \end{center} |
180 \end{center} |
183 \end{figure} |
181 \end{figure} |
184 *} |
182 *} |
185 |
183 |
186 instance monoid < semigroup |
184 instance monoid < semigroup |
187 proof intro_classes |
185 proof intro_classes |
188 fix x y z :: "'a\\<Colon>monoid" |
186 fix x y z :: "'a\<Colon>monoid" |
189 show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)" |
187 show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)" |
190 by (rule monoid.assoc) |
188 by (rule monoid.assoc) |
191 qed |
189 qed |
192 |
190 |
193 instance group < monoid |
191 instance group < monoid |
194 proof intro_classes |
192 proof intro_classes |
195 fix x y z :: "'a\\<Colon>group" |
193 fix x y z :: "'a\<Colon>group" |
196 show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)" |
194 show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)" |
197 by (rule semigroup.assoc) |
195 by (rule semigroup.assoc) |
198 show "\<unit> \<Otimes> x = x" |
196 show "\<unit> \<odot> x = x" |
199 by (rule group.left_unit) |
197 by (rule group.left_unit) |
200 show "x \<Otimes> \<unit> = x" |
198 show "x \<odot> \<unit> = x" |
201 by (rule group_right_unit) |
199 by (rule group_right_unit) |
202 qed |
200 qed |
203 |
201 |
204 text {* |
202 text {* |
205 \medskip The $\isakeyword{instance}$ command sets up an appropriate |
203 \medskip The $\isakeyword{instance}$ command sets up an appropriate |
206 goal that represents the class inclusion (or type arity, see |
204 goal that represents the class inclusion (or type arity, see |
207 \secref{sec:inst-arity}) to be proven |
205 \secref{sec:inst-arity}) to be proven (see also |
208 (see also \cite{isabelle-isar-ref}). The $intro_classes$ proof |
206 \cite{isabelle-isar-ref}). The @{text intro_classes} proof method |
209 method does back-chaining of class membership statements wrt.\ the |
207 does back-chaining of class membership statements wrt.\ the hierarchy |
210 hierarchy of any classes defined in the current theory; the effect is |
208 of any classes defined in the current theory; the effect is to reduce |
211 to reduce to the initial statement to a number of goals that directly |
209 to the initial statement to a number of goals that directly |
212 correspond to any class axioms encountered on the path upwards |
210 correspond to any class axioms encountered on the path upwards |
213 through the class hierarchy. |
211 through the class hierarchy. |
214 *} |
212 *} |
215 |
213 |
216 |
214 |