2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Group}% |
3 \def\isabellecontext{Group}% |
4 % |
4 % |
5 \isamarkupheader{Basic group theory% |
5 \isamarkupheader{Basic group theory% |
6 } |
6 } |
7 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}% |
7 \isamarkuptrue% |
|
8 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
|
9 % |
8 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
9 \medskip\noindent The meta-level type system of Isabelle supports |
11 \medskip\noindent The meta-level type system of Isabelle supports |
10 \emph{intersections} and \emph{inclusions} of type classes. These |
12 \emph{intersections} and \emph{inclusions} of type classes. These |
11 directly correspond to intersections and inclusions of type |
13 directly correspond to intersections and inclusions of type |
12 predicates in a purely set theoretic sense. This is sufficient as a |
14 predicates in a purely set theoretic sense. This is sufficient as a |
13 means to describe simple hierarchies of structures. As an |
15 means to describe simple hierarchies of structures. As an |
14 illustration, we use the well-known example of semigroups, monoids, |
16 illustration, we use the well-known example of semigroups, monoids, |
15 general groups and Abelian groups.% |
17 general groups and Abelian groups.% |
16 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
|
19 \isamarkuptrue% |
17 % |
20 % |
18 \isamarkupsubsection{Monoids and Groups% |
21 \isamarkupsubsection{Monoids and Groups% |
19 } |
22 } |
|
23 \isamarkuptrue% |
20 % |
24 % |
21 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
22 First we declare some polymorphic constants required later for the |
26 First we declare some polymorphic constants required later for the |
23 signature parts of our structures.% |
27 signature parts of our structures.% |
24 \end{isamarkuptext}% |
28 \end{isamarkuptext}% |
|
29 \isamarkuptrue% |
25 \isacommand{consts}\isanewline |
30 \isacommand{consts}\isanewline |
26 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
31 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
27 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
32 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
28 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}% |
33 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
|
34 % |
29 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
30 \noindent Next we define class \isa{monoid} of monoids with |
36 \noindent Next we define class \isa{monoid} of monoids with |
31 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
37 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
32 axioms are allowed for user convenience --- they simply represent the |
38 axioms are allowed for user convenience --- they simply represent the |
33 conjunction of their respective universal closures.% |
39 conjunction of their respective universal closures.% |
34 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
|
41 \isamarkuptrue% |
35 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
42 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
36 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
43 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
37 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
44 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
38 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}% |
45 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% |
|
46 % |
39 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
40 \noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are |
48 \noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are |
41 specified appropriately, such that \isa{{\isasymodot}} is associative and |
49 specified appropriately, such that \isa{{\isasymodot}} is associative and |
42 \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}} |
50 \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}} |
43 operation.% |
51 operation.% |
44 \end{isamarkuptext}% |
52 \end{isamarkuptext}% |
|
53 \isamarkuptrue% |
45 % |
54 % |
46 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
47 \medskip Independently of \isa{monoid}, we now define a linear |
56 \medskip Independently of \isa{monoid}, we now define a linear |
48 hierarchy of semigroups, general groups and Abelian groups. Note |
57 hierarchy of semigroups, general groups and Abelian groups. Note |
49 that the names of class axioms are automatically qualified with each |
58 that the names of class axioms are automatically qualified with each |
50 class name, so we may re-use common names such as \isa{assoc}.% |
59 class name, so we may re-use common names such as \isa{assoc}.% |
51 \end{isamarkuptext}% |
60 \end{isamarkuptext}% |
|
61 \isamarkuptrue% |
52 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
62 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
53 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
63 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
54 \isanewline |
64 \isanewline |
|
65 \isamarkupfalse% |
55 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
66 \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline |
56 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
67 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
57 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
68 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
58 \isanewline |
69 \isanewline |
|
70 \isamarkupfalse% |
59 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
71 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline |
60 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}% |
72 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% |
|
73 % |
61 \begin{isamarkuptext}% |
74 \begin{isamarkuptext}% |
62 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
75 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} |
63 from \isa{semigroup} and adds two further group axioms. Similarly, |
76 from \isa{semigroup} and adds two further group axioms. Similarly, |
64 \isa{agroup} is defined as the subset of \isa{group} such that |
77 \isa{agroup} is defined as the subset of \isa{group} such that |
65 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
78 for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% |
66 \end{isamarkuptext}% |
79 \end{isamarkuptext}% |
|
80 \isamarkuptrue% |
67 % |
81 % |
68 \isamarkupsubsection{Abstract reasoning% |
82 \isamarkupsubsection{Abstract reasoning% |
69 } |
83 } |
|
84 \isamarkuptrue% |
70 % |
85 % |
71 \begin{isamarkuptext}% |
86 \begin{isamarkuptext}% |
72 In a sense, axiomatic type classes may be viewed as \emph{abstract |
87 In a sense, axiomatic type classes may be viewed as \emph{abstract |
73 theories}. Above class definitions gives rise to abstract axioms |
88 theories}. Above class definitions gives rise to abstract axioms |
74 \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} |
89 \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} |
82 ordinary Isabelle theorems, which may be used in proofs without |
97 ordinary Isabelle theorems, which may be used in proofs without |
83 special treatment. Such ``abstract proofs'' usually yield new |
98 special treatment. Such ``abstract proofs'' usually yield new |
84 ``abstract theorems''. For example, we may now derive the following |
99 ``abstract theorems''. For example, we may now derive the following |
85 well-known laws of general groups.% |
100 well-known laws of general groups.% |
86 \end{isamarkuptext}% |
101 \end{isamarkuptext}% |
|
102 \isamarkuptrue% |
87 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
103 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
|
104 \isamarkupfalse% |
88 \isacommand{proof}\ {\isacharminus}\isanewline |
105 \isacommand{proof}\ {\isacharminus}\isanewline |
89 \ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
106 \ \ \isamarkupfalse% |
90 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
107 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
91 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
108 \ \ \ \ \isamarkupfalse% |
92 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
109 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
93 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
110 \ \ \isamarkupfalse% |
94 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
111 \isacommand{also}\ \isamarkupfalse% |
95 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
112 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
96 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
113 \ \ \ \ \isamarkupfalse% |
97 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
114 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
98 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
115 \ \ \isamarkupfalse% |
99 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
116 \isacommand{also}\ \isamarkupfalse% |
100 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
117 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
101 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
118 \ \ \ \ \isamarkupfalse% |
102 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
119 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
103 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
120 \ \ \isamarkupfalse% |
104 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
121 \isacommand{also}\ \isamarkupfalse% |
105 \ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline |
122 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
106 \isacommand{qed}% |
123 \ \ \ \ \isamarkupfalse% |
|
124 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
125 \ \ \isamarkupfalse% |
|
126 \isacommand{also}\ \isamarkupfalse% |
|
127 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
|
128 \ \ \ \ \isamarkupfalse% |
|
129 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
130 \ \ \isamarkupfalse% |
|
131 \isacommand{also}\ \isamarkupfalse% |
|
132 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline |
|
133 \ \ \ \ \isamarkupfalse% |
|
134 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
135 \ \ \isamarkupfalse% |
|
136 \isacommand{also}\ \isamarkupfalse% |
|
137 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline |
|
138 \ \ \ \ \isamarkupfalse% |
|
139 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
140 \ \ \isamarkupfalse% |
|
141 \isacommand{also}\ \isamarkupfalse% |
|
142 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline |
|
143 \ \ \ \ \isamarkupfalse% |
|
144 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
145 \ \ \isamarkupfalse% |
|
146 \isacommand{finally}\ \isamarkupfalse% |
|
147 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
148 \isacommand{{\isachardot}}\isanewline |
|
149 \isamarkupfalse% |
|
150 \isacommand{qed}\isamarkupfalse% |
|
151 % |
107 \begin{isamarkuptext}% |
152 \begin{isamarkuptext}% |
108 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established much |
153 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established much |
109 easier.% |
154 easier.% |
110 \end{isamarkuptext}% |
155 \end{isamarkuptext}% |
|
156 \isamarkuptrue% |
111 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
157 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline |
|
158 \isamarkupfalse% |
112 \isacommand{proof}\ {\isacharminus}\isanewline |
159 \isacommand{proof}\ {\isacharminus}\isanewline |
113 \ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
160 \ \ \isamarkupfalse% |
114 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
161 \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline |
115 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
162 \ \ \ \ \isamarkupfalse% |
116 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
163 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline |
117 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
164 \ \ \isamarkupfalse% |
118 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
165 \isacommand{also}\ \isamarkupfalse% |
119 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
166 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
120 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
167 \ \ \ \ \isamarkupfalse% |
121 \ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline |
168 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
122 \isacommand{qed}% |
169 \ \ \isamarkupfalse% |
|
170 \isacommand{also}\ \isamarkupfalse% |
|
171 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline |
|
172 \ \ \ \ \isamarkupfalse% |
|
173 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline |
|
174 \ \ \isamarkupfalse% |
|
175 \isacommand{also}\ \isamarkupfalse% |
|
176 \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
|
177 \ \ \ \ \isamarkupfalse% |
|
178 \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
179 \ \ \isamarkupfalse% |
|
180 \isacommand{finally}\ \isamarkupfalse% |
|
181 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
182 \isacommand{{\isachardot}}\isanewline |
|
183 \isamarkupfalse% |
|
184 \isacommand{qed}\isamarkupfalse% |
|
185 % |
123 \begin{isamarkuptext}% |
186 \begin{isamarkuptext}% |
124 \medskip Abstract theorems may be instantiated to only those types |
187 \medskip Abstract theorems may be instantiated to only those types |
125 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
188 \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is |
126 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}.% |
189 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}.% |
127 \end{isamarkuptext}% |
190 \end{isamarkuptext}% |
|
191 \isamarkuptrue% |
128 % |
192 % |
129 \isamarkupsubsection{Abstract instantiation% |
193 \isamarkupsubsection{Abstract instantiation% |
130 } |
194 } |
|
195 \isamarkuptrue% |
131 % |
196 % |
132 \begin{isamarkuptext}% |
197 \begin{isamarkuptext}% |
133 From the definition, the \isa{monoid} and \isa{group} classes |
198 From the definition, the \isa{monoid} and \isa{group} classes |
134 have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} had |
199 have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} had |
135 to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} |
200 to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} |
163 \caption{Monoids and groups: according to definition, and by proof} |
228 \caption{Monoids and groups: according to definition, and by proof} |
164 \label{fig:monoid-group} |
229 \label{fig:monoid-group} |
165 \end{center} |
230 \end{center} |
166 \end{figure}% |
231 \end{figure}% |
167 \end{isamarkuptext}% |
232 \end{isamarkuptext}% |
|
233 \isamarkuptrue% |
168 \isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
234 \isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline |
|
235 \isamarkupfalse% |
169 \isacommand{proof}\isanewline |
236 \isacommand{proof}\isanewline |
170 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline |
237 \ \ \isamarkupfalse% |
171 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
238 \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline |
172 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline |
239 \ \ \isamarkupfalse% |
|
240 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
|
241 \ \ \ \ \isamarkupfalse% |
|
242 \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline |
|
243 \isamarkupfalse% |
173 \isacommand{qed}\isanewline |
244 \isacommand{qed}\isanewline |
174 \isanewline |
245 \isanewline |
|
246 \isamarkupfalse% |
175 \isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline |
247 \isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline |
|
248 \isamarkupfalse% |
176 \isacommand{proof}\isanewline |
249 \isacommand{proof}\isanewline |
177 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline |
250 \ \ \isamarkupfalse% |
178 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
251 \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline |
179 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
252 \ \ \isamarkupfalse% |
180 \ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
253 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline |
181 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
254 \ \ \ \ \isamarkupfalse% |
182 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
255 \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
183 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
256 \ \ \isamarkupfalse% |
184 \isacommand{qed}% |
257 \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
|
258 \ \ \ \ \isamarkupfalse% |
|
259 \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
260 \ \ \isamarkupfalse% |
|
261 \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
|
262 \ \ \ \ \isamarkupfalse% |
|
263 \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline |
|
264 \isamarkupfalse% |
|
265 \isacommand{qed}\isamarkupfalse% |
|
266 % |
185 \begin{isamarkuptext}% |
267 \begin{isamarkuptext}% |
186 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
268 \medskip The $\INSTANCE$ command sets up an appropriate goal that |
187 represents the class inclusion (or type arity, see |
269 represents the class inclusion (or type arity, see |
188 \secref{sec:inst-arity}) to be proven (see also |
270 \secref{sec:inst-arity}) to be proven (see also |
189 \cite{isabelle-isar-ref}). The initial proof step causes |
271 \cite{isabelle-isar-ref}). The initial proof step causes |
208 |
292 |
209 \medskip As a typical example, we show that type \isa{bool} with |
293 \medskip As a typical example, we show that type \isa{bool} with |
210 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
294 exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and |
211 \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% |
295 \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% |
212 \end{isamarkuptext}% |
296 \end{isamarkuptext}% |
|
297 \isamarkuptrue% |
213 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
298 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
214 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
299 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline |
215 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
300 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline |
216 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}% |
301 \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% |
|
302 % |
217 \begin{isamarkuptext}% |
303 \begin{isamarkuptext}% |
218 \medskip It is important to note that above $\DEFS$ are just |
304 \medskip It is important to note that above $\DEFS$ are just |
219 overloaded meta-level constant definitions, where type classes are |
305 overloaded meta-level constant definitions, where type classes are |
220 not yet involved at all. This form of constant definition with |
306 not yet involved at all. This form of constant definition with |
221 overloading (and optional recursion over the syntactic structure of |
307 overloading (and optional recursion over the syntactic structure of |
226 |
312 |
227 \medskip Since we have chosen above $\DEFS$ of the generic group |
313 \medskip Since we have chosen above $\DEFS$ of the generic group |
228 operations on type \isa{bool} appropriately, the class membership |
314 operations on type \isa{bool} appropriately, the class membership |
229 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
315 \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% |
230 \end{isamarkuptext}% |
316 \end{isamarkuptext}% |
|
317 \isamarkuptrue% |
231 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
318 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline |
|
319 \isamarkupfalse% |
232 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
320 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline |
233 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
321 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline |
234 \ \ \isacommand{fix}\ x\ y\ z\isanewline |
322 \ \ \isamarkupfalse% |
235 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
323 \isacommand{fix}\ x\ y\ z\isanewline |
236 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
324 \ \ \isamarkupfalse% |
237 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
325 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
238 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline |
326 \isacommand{by}\ blast\isanewline |
239 \isacommand{qed}% |
327 \ \ \isamarkupfalse% |
|
328 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isamarkupfalse% |
|
329 \isacommand{by}\ blast\isanewline |
|
330 \ \ \isamarkupfalse% |
|
331 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isamarkupfalse% |
|
332 \isacommand{by}\ blast\isanewline |
|
333 \ \ \isamarkupfalse% |
|
334 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
|
335 \isacommand{by}\ blast\isanewline |
|
336 \isamarkupfalse% |
|
337 \isacommand{qed}\isamarkupfalse% |
|
338 % |
240 \begin{isamarkuptext}% |
339 \begin{isamarkuptext}% |
241 The result of an $\INSTANCE$ statement is both expressed as a theorem |
340 The result of an $\INSTANCE$ statement is both expressed as a theorem |
242 of Isabelle's meta-logic, and as a type arity of the type signature. |
341 of Isabelle's meta-logic, and as a type arity of the type signature. |
243 The latter enables type-inference system to take care of this new |
342 The latter enables type-inference system to take care of this new |
244 instance automatically. |
343 instance automatically. |
265 |
366 |
266 This feature enables us to \emph{lift operations}, say to Cartesian |
367 This feature enables us to \emph{lift operations}, say to Cartesian |
267 products, direct sums or function spaces. Subsequently we lift |
368 products, direct sums or function spaces. Subsequently we lift |
268 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
369 \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% |
269 \end{isamarkuptext}% |
370 \end{isamarkuptext}% |
|
371 \isamarkuptrue% |
270 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
372 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
271 \ \ 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}% |
373 \ \ 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% |
|
374 % |
272 \begin{isamarkuptext}% |
375 \begin{isamarkuptext}% |
273 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
376 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} |
274 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 to |
377 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 to |
275 semigroups. This may be established formally as follows.% |
378 semigroups. This may be established formally as follows.% |
276 \end{isamarkuptext}% |
379 \end{isamarkuptext}% |
|
380 \isamarkuptrue% |
277 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
381 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
|
382 \isamarkupfalse% |
278 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
383 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline |
279 \ \ \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline |
384 \ \ \isamarkupfalse% |
280 \ \ \isacommand{show}\isanewline |
385 \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline |
|
386 \ \ \isamarkupfalse% |
|
387 \isacommand{show}\isanewline |
281 \ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
388 \ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline |
282 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
389 \ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline |
283 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
390 \ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline |
284 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
391 \ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
285 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
392 \ \ \ \ \isamarkupfalse% |
286 \isacommand{qed}% |
393 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline |
|
394 \isamarkupfalse% |
|
395 \isacommand{qed}\isamarkupfalse% |
|
396 % |
287 \begin{isamarkuptext}% |
397 \begin{isamarkuptext}% |
288 Thus, if we view class instances as ``structures'', then overloaded |
398 Thus, if we view class instances as ``structures'', then overloaded |
289 constant definitions with recursion over types indirectly provide |
399 constant definitions with recursion over types indirectly provide |
290 some kind of ``functors'' --- i.e.\ mappings between abstract |
400 some kind of ``functors'' --- i.e.\ mappings between abstract |
291 theories.% |
401 theories.% |
292 \end{isamarkuptext}% |
402 \end{isamarkuptext}% |
293 \isacommand{end}\end{isabellebody}% |
403 \isamarkuptrue% |
|
404 \isacommand{end}\isamarkupfalse% |
|
405 \end{isabellebody}% |
294 %%% Local Variables: |
406 %%% Local Variables: |
295 %%% mode: latex |
407 %%% mode: latex |
296 %%% TeX-master: "root" |
408 %%% TeX-master: "root" |
297 %%% End: |
409 %%% End: |