author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12344 | 7237c6497cb1 |
child 17132 | 153fe83804c9 |
permissions | -rw-r--r-- |
9767 | 1 |
% |
2 |
\begin{isabellebody}% |
|
9921 | 3 |
\def\isabellecontext{Group}% |
8903 | 4 |
% |
10395 | 5 |
\isamarkupheader{Basic group theory% |
6 |
} |
|
11964 | 7 |
\isamarkuptrue% |
8 |
\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
|
9 |
% |
|
8903 | 10 |
\begin{isamarkuptext}% |
10140 | 11 |
\medskip\noindent The meta-level type system of Isabelle supports |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
12 |
\emph{intersections} and \emph{inclusions} of type classes. These |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
13 |
directly correspond to intersections and inclusions of type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
14 |
predicates in a purely set theoretic sense. This is sufficient as a |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
15 |
means to describe simple hierarchies of structures. As an |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
16 |
illustration, we use the well-known example of semigroups, monoids, |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
17 |
general groups and Abelian groups.% |
8903 | 18 |
\end{isamarkuptext}% |
11964 | 19 |
\isamarkuptrue% |
8903 | 20 |
% |
10395 | 21 |
\isamarkupsubsection{Monoids and Groups% |
22 |
} |
|
11964 | 23 |
\isamarkuptrue% |
8903 | 24 |
% |
25 |
\begin{isamarkuptext}% |
|
26 |
First we declare some polymorphic constants required later for the |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
27 |
signature parts of our structures.% |
8903 | 28 |
\end{isamarkuptext}% |
11964 | 29 |
\isamarkuptrue% |
8890 | 30 |
\isacommand{consts}\isanewline |
10207 | 31 |
\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
11071 | 32 |
\ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
12344 | 33 |
\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
11964 | 34 |
% |
8903 | 35 |
\begin{isamarkuptext}% |
10140 | 36 |
\noindent Next we define class \isa{monoid} of monoids with |
12344 | 37 |
operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
38 |
axioms are allowed for user convenience --- they simply represent |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
39 |
the conjunction of their respective universal closures.% |
8903 | 40 |
\end{isamarkuptext}% |
11964 | 41 |
\isamarkuptrue% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
42 |
\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline |
10140 | 43 |
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
12344 | 44 |
\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
45 |
\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
|
11964 | 46 |
% |
8903 | 47 |
\begin{isamarkuptext}% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
48 |
\noindent So class \isa{monoid} contains exactly those types |
12344 | 49 |
\isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
50 |
are specified appropriately, such that \isa{{\isasymodot}} is associative and |
12344 | 51 |
\isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
52 |
operation.% |
8903 | 53 |
\end{isamarkuptext}% |
11964 | 54 |
\isamarkuptrue% |
8903 | 55 |
% |
56 |
\begin{isamarkuptext}% |
|
10140 | 57 |
\medskip Independently of \isa{monoid}, we now define a linear |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
58 |
hierarchy of semigroups, general groups and Abelian groups. Note |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
59 |
that the names of class axioms are automatically qualified with each |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
60 |
class name, so we may re-use common names such as \isa{assoc}.% |
8903 | 61 |
\end{isamarkuptext}% |
11964 | 62 |
\isamarkuptrue% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
63 |
\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
10140 | 64 |
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
8890 | 65 |
\isanewline |
11964 | 66 |
\isamarkupfalse% |
11099 | 67 |
\isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
12344 | 68 |
\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
69 |
\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
|
8903 | 70 |
\isanewline |
11964 | 71 |
\isamarkupfalse% |
11099 | 72 |
\isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
11964 | 73 |
\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
74 |
% |
|
8903 | 75 |
\begin{isamarkuptext}% |
10140 | 76 |
\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
77 |
from \isa{semigroup} and adds two further group axioms. Similarly, |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
78 |
\isa{agroup} is defined as the subset of \isa{group} such that |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
79 |
for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
8903 | 80 |
\end{isamarkuptext}% |
11964 | 81 |
\isamarkuptrue% |
8903 | 82 |
% |
10395 | 83 |
\isamarkupsubsection{Abstract reasoning% |
84 |
} |
|
11964 | 85 |
\isamarkuptrue% |
8903 | 86 |
% |
8890 | 87 |
\begin{isamarkuptext}% |
8903 | 88 |
In a sense, axiomatic type classes may be viewed as \emph{abstract |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
89 |
theories}. Above class definitions gives rise to abstract axioms |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
90 |
\isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}. \emph{Sort constraints} like this express a logical |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
91 |
precondition for the whole formula. For example, \isa{assoc} |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
92 |
states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative. |
8903 | 93 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
94 |
\medskip From a technical point of view, abstract axioms are just |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
95 |
ordinary Isabelle theorems, which may be used in proofs without |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
96 |
special treatment. Such ``abstract proofs'' usually yield new |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
97 |
``abstract theorems''. For example, we may now derive the following |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
98 |
well-known laws of general groups.% |
8890 | 99 |
\end{isamarkuptext}% |
11964 | 100 |
\isamarkuptrue% |
12344 | 101 |
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
11964 | 102 |
\isamarkupfalse% |
9665 | 103 |
\isacommand{proof}\ {\isacharminus}\isanewline |
11964 | 104 |
\ \ \isamarkupfalse% |
12344 | 105 |
\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
11964 | 106 |
\ \ \ \ \isamarkupfalse% |
107 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
108 |
\ \ \isamarkupfalse% |
|
109 |
\isacommand{also}\ \isamarkupfalse% |
|
12344 | 110 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
11964 | 111 |
\ \ \ \ \isamarkupfalse% |
112 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
113 |
\ \ \isamarkupfalse% |
|
114 |
\isacommand{also}\ \isamarkupfalse% |
|
115 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
|
116 |
\ \ \ \ \isamarkupfalse% |
|
117 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
118 |
\ \ \isamarkupfalse% |
|
119 |
\isacommand{also}\ \isamarkupfalse% |
|
120 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
|
121 |
\ \ \ \ \isamarkupfalse% |
|
122 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
123 |
\ \ \isamarkupfalse% |
|
124 |
\isacommand{also}\ \isamarkupfalse% |
|
12344 | 125 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
11964 | 126 |
\ \ \ \ \isamarkupfalse% |
127 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
128 |
\ \ \isamarkupfalse% |
|
129 |
\isacommand{also}\ \isamarkupfalse% |
|
12344 | 130 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
11964 | 131 |
\ \ \ \ \isamarkupfalse% |
132 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
133 |
\ \ \isamarkupfalse% |
|
134 |
\isacommand{also}\ \isamarkupfalse% |
|
135 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
|
136 |
\ \ \ \ \isamarkupfalse% |
|
137 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
138 |
\ \ \isamarkupfalse% |
|
139 |
\isacommand{also}\ \isamarkupfalse% |
|
12344 | 140 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline |
11964 | 141 |
\ \ \ \ \isamarkupfalse% |
142 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
143 |
\ \ \isamarkupfalse% |
|
144 |
\isacommand{finally}\ \isamarkupfalse% |
|
145 |
\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
146 |
\isacommand{{\isachardot}}\isanewline |
|
147 |
\isamarkupfalse% |
|
148 |
\isacommand{qed}\isamarkupfalse% |
|
149 |
% |
|
8890 | 150 |
\begin{isamarkuptext}% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
151 |
\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
152 |
much easier.% |
8890 | 153 |
\end{isamarkuptext}% |
11964 | 154 |
\isamarkuptrue% |
12344 | 155 |
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
11964 | 156 |
\isamarkupfalse% |
9665 | 157 |
\isacommand{proof}\ {\isacharminus}\isanewline |
11964 | 158 |
\ \ \isamarkupfalse% |
12344 | 159 |
\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
11964 | 160 |
\ \ \ \ \isamarkupfalse% |
161 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
162 |
\ \ \isamarkupfalse% |
|
163 |
\isacommand{also}\ \isamarkupfalse% |
|
164 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
|
165 |
\ \ \ \ \isamarkupfalse% |
|
166 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
167 |
\ \ \isamarkupfalse% |
|
168 |
\isacommand{also}\ \isamarkupfalse% |
|
12344 | 169 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
11964 | 170 |
\ \ \ \ \isamarkupfalse% |
171 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
172 |
\ \ \isamarkupfalse% |
|
173 |
\isacommand{also}\ \isamarkupfalse% |
|
174 |
\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
|
175 |
\ \ \ \ \isamarkupfalse% |
|
176 |
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
177 |
\ \ \isamarkupfalse% |
|
178 |
\isacommand{finally}\ \isamarkupfalse% |
|
179 |
\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
180 |
\isacommand{{\isachardot}}\isanewline |
|
181 |
\isamarkupfalse% |
|
182 |
\isacommand{qed}\isamarkupfalse% |
|
183 |
% |
|
8903 | 184 |
\begin{isamarkuptext}% |
185 |
\medskip Abstract theorems may be instantiated to only those types |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
186 |
\isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
187 |
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}.% |
8903 | 188 |
\end{isamarkuptext}% |
11964 | 189 |
\isamarkuptrue% |
8903 | 190 |
% |
10395 | 191 |
\isamarkupsubsection{Abstract instantiation% |
192 |
} |
|
11964 | 193 |
\isamarkuptrue% |
8903 | 194 |
% |
195 |
\begin{isamarkuptext}% |
|
10140 | 196 |
From the definition, the \isa{monoid} and \isa{group} classes |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
197 |
have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
198 |
had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
199 |
axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
200 |
theory (see page~\pageref{thm:group-right-unit}), we may now |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
201 |
instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}). |
8903 | 202 |
|
203 |
\begin{figure}[htbp] |
|
204 |
\begin{center} |
|
205 |
\small |
|
206 |
\unitlength 0.6mm |
|
207 |
\begin{picture}(65,90)(0,-10) |
|
208 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
209 |
\put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} |
|
10140 | 210 |
\put(15,5){\makebox(0,0){\isa{agroup}}} |
211 |
\put(15,25){\makebox(0,0){\isa{group}}} |
|
212 |
\put(15,45){\makebox(0,0){\isa{semigroup}}} |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
213 |
\put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}} |
8903 | 214 |
\end{picture} |
215 |
\hspace{4em} |
|
216 |
\begin{picture}(30,90)(0,0) |
|
217 |
\put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} |
|
218 |
\put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} |
|
10140 | 219 |
\put(15,5){\makebox(0,0){\isa{agroup}}} |
220 |
\put(15,25){\makebox(0,0){\isa{group}}} |
|
221 |
\put(15,45){\makebox(0,0){\isa{monoid}}} |
|
222 |
\put(15,65){\makebox(0,0){\isa{semigroup}}} |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
223 |
\put(15,85){\makebox(0,0){\isa{type}}} |
8903 | 224 |
\end{picture} |
225 |
\caption{Monoids and groups: according to definition, and by proof} |
|
226 |
\label{fig:monoid-group} |
|
227 |
\end{center} |
|
8907 | 228 |
\end{figure}% |
8903 | 229 |
\end{isamarkuptext}% |
11964 | 230 |
\isamarkuptrue% |
11099 | 231 |
\isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
11964 | 232 |
\isamarkupfalse% |
10310 | 233 |
\isacommand{proof}\isanewline |
11964 | 234 |
\ \ \isamarkupfalse% |
235 |
\isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline |
|
236 |
\ \ \isamarkupfalse% |
|
237 |
\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
|
238 |
\ \ \ \ \isamarkupfalse% |
|
239 |
\isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline |
|
240 |
\isamarkupfalse% |
|
8890 | 241 |
\isacommand{qed}\isanewline |
242 |
\isanewline |
|
11964 | 243 |
\isamarkupfalse% |
11099 | 244 |
\isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline |
11964 | 245 |
\isamarkupfalse% |
10310 | 246 |
\isacommand{proof}\isanewline |
11964 | 247 |
\ \ \isamarkupfalse% |
248 |
\isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline |
|
249 |
\ \ \isamarkupfalse% |
|
250 |
\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
|
251 |
\ \ \ \ \isamarkupfalse% |
|
252 |
\isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
253 |
\ \ \isamarkupfalse% |
|
12344 | 254 |
\isacommand{show}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
11964 | 255 |
\ \ \ \ \isamarkupfalse% |
256 |
\isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
257 |
\ \ \isamarkupfalse% |
|
12344 | 258 |
\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
11964 | 259 |
\ \ \ \ \isamarkupfalse% |
260 |
\isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
261 |
\isamarkupfalse% |
|
262 |
\isacommand{qed}\isamarkupfalse% |
|
263 |
% |
|
8903 | 264 |
\begin{isamarkuptext}% |
10223 | 265 |
\medskip The $\INSTANCE$ command sets up an appropriate goal that |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
266 |
represents the class inclusion (or type arity, see |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
267 |
\secref{sec:inst-arity}) to be proven (see also |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
268 |
\cite{isabelle-isar-ref}). The initial proof step causes |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
269 |
back-chaining of class membership statements wrt.\ the hierarchy of |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
270 |
any classes defined in the current theory; the effect is to reduce |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
271 |
to the initial statement to a number of goals that directly |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
272 |
correspond to any class axioms encountered on the path upwards |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
273 |
through the class hierarchy.% |
8903 | 274 |
\end{isamarkuptext}% |
11964 | 275 |
\isamarkuptrue% |
8903 | 276 |
% |
10395 | 277 |
\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}% |
278 |
} |
|
11964 | 279 |
\isamarkuptrue% |
8903 | 280 |
% |
281 |
\begin{isamarkuptext}% |
|
11099 | 282 |
So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} --- |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
283 |
$c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
284 |
of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
285 |
applications are \emph{concrete instantiations} of axiomatic type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
286 |
classes. That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be established at the |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
287 |
logical level and then transferred to Isabelle's type signature |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
288 |
level. |
8903 | 289 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
290 |
\medskip As a typical example, we show that type \isa{bool} with |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
291 |
exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
12344 | 292 |
\isa{False} as \isa{{\isasymone}} forms an Abelian group.% |
8903 | 293 |
\end{isamarkuptext}% |
11964 | 294 |
\isamarkuptrue% |
9665 | 295 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
10140 | 296 |
\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
9672 | 297 |
\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
12344 | 298 |
\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
11964 | 299 |
% |
8903 | 300 |
\begin{isamarkuptext}% |
301 |
\medskip It is important to note that above $\DEFS$ are just |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
302 |
overloaded meta-level constant definitions, where type classes are |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
303 |
not yet involved at all. This form of constant definition with |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
304 |
overloading (and optional recursion over the syntactic structure of |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
305 |
simple types) are admissible as definitional extensions of plain HOL |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
306 |
\cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
307 |
required for overloading. Nevertheless, overloaded definitions are |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
308 |
best applied in the context of type classes. |
8903 | 309 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
310 |
\medskip Since we have chosen above $\DEFS$ of the generic group |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
311 |
operations on type \isa{bool} appropriately, the class membership |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
312 |
\isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
8903 | 313 |
\end{isamarkuptext}% |
11964 | 314 |
\isamarkuptrue% |
9672 | 315 |
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
11964 | 316 |
\isamarkupfalse% |
9672 | 317 |
\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
9665 | 318 |
\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
11964 | 319 |
\ \ \isamarkupfalse% |
320 |
\isacommand{fix}\ x\ y\ z\isanewline |
|
321 |
\ \ \isamarkupfalse% |
|
322 |
\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
|
323 |
\isacommand{by}\ blast\isanewline |
|
324 |
\ \ \isamarkupfalse% |
|
325 |
\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isamarkupfalse% |
|
326 |
\isacommand{by}\ blast\isanewline |
|
327 |
\ \ \isamarkupfalse% |
|
328 |
\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isamarkupfalse% |
|
329 |
\isacommand{by}\ blast\isanewline |
|
330 |
\ \ \isamarkupfalse% |
|
331 |
\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
|
332 |
\isacommand{by}\ blast\isanewline |
|
333 |
\isamarkupfalse% |
|
334 |
\isacommand{qed}\isamarkupfalse% |
|
335 |
% |
|
8903 | 336 |
\begin{isamarkuptext}% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
337 |
The result of an $\INSTANCE$ statement is both expressed as a |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
338 |
theorem of Isabelle's meta-logic, and as a type arity of the type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
339 |
signature. The latter enables type-inference system to take care of |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
340 |
this new instance automatically. |
8903 | 341 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
342 |
\medskip We could now also instantiate our group theory classes to |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
343 |
many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
344 |
(e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation |
12344 | 345 |
and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
346 |
(e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the |
12344 | 347 |
characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
348 |
really become overloaded, i.e.\ have different meanings on different |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
349 |
types.% |
8903 | 350 |
\end{isamarkuptext}% |
11964 | 351 |
\isamarkuptrue% |
8903 | 352 |
% |
10395 | 353 |
\isamarkupsubsection{Lifting and Functors% |
354 |
} |
|
11964 | 355 |
\isamarkuptrue% |
8903 | 356 |
% |
357 |
\begin{isamarkuptext}% |
|
358 |
As already mentioned above, overloading in the simply-typed HOL |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
359 |
systems may include recursion over the syntactic structure of types. |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
360 |
That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
361 |
contain constants of name \isa{c} on the right-hand side --- if |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
362 |
these have types that are structurally simpler than \isa{{\isasymtau}}. |
8903 | 363 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
364 |
This feature enables us to \emph{lift operations}, say to Cartesian |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
365 |
products, direct sums or function spaces. Subsequently we lift |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
366 |
\isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
8903 | 367 |
\end{isamarkuptext}% |
11964 | 368 |
\isamarkuptrue% |
9665 | 369 |
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
11964 | 370 |
\ \ 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}\isamarkupfalse% |
371 |
% |
|
8903 | 372 |
\begin{isamarkuptext}% |
10140 | 373 |
It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
374 |
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 |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
375 |
to semigroups. This may be established formally as follows.% |
8903 | 376 |
\end{isamarkuptext}% |
11964 | 377 |
\isamarkuptrue% |
9672 | 378 |
\isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
11964 | 379 |
\isamarkupfalse% |
9672 | 380 |
\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
11964 | 381 |
\ \ \isamarkupfalse% |
382 |
\isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline |
|
383 |
\ \ \isamarkupfalse% |
|
384 |
\isacommand{show}\isanewline |
|
10140 | 385 |
\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
386 |
\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
|
387 |
\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
|
388 |
\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
|
11964 | 389 |
\ \ \ \ \isamarkupfalse% |
390 |
\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
391 |
\isamarkupfalse% |
|
392 |
\isacommand{qed}\isamarkupfalse% |
|
393 |
% |
|
8903 | 394 |
\begin{isamarkuptext}% |
395 |
Thus, if we view class instances as ``structures'', then overloaded |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
396 |
constant definitions with recursion over types indirectly provide |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
397 |
some kind of ``functors'' --- i.e.\ mappings between abstract |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
398 |
theories.% |
8903 | 399 |
\end{isamarkuptext}% |
11964 | 400 |
\isamarkuptrue% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
401 |
\isacommand{end}\isanewline |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
402 |
\isamarkupfalse% |
11964 | 403 |
\end{isabellebody}% |
9145 | 404 |
%%% Local Variables: |
405 |
%%% mode: latex |
|
406 |
%%% TeX-master: "root" |
|
407 |
%%% End: |