src/HOL/Isar_Examples/Group.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 37671 fa53d267dab3 child 55656 eb07b0acbebc permissions -rw-r--r--
 wenzelm@33026 1 (* Title: HOL/Isar_Examples/Group.thy wenzelm@6763 2 Author: Markus Wenzel, TU Muenchen wenzelm@6763 3 *) wenzelm@6763 4 wenzelm@10007 5 header {* Basic group theory *} wenzelm@7748 6 wenzelm@31758 7 theory Group wenzelm@31758 8 imports Main wenzelm@31758 9 begin wenzelm@6763 10 wenzelm@10007 11 subsection {* Groups and calculational reasoning *} wenzelm@6784 12 wenzelm@37671 13 text {* Groups over signature $({\times} :: \alpha \To \alpha \To wenzelm@37671 14 \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ wenzelm@37671 15 are defined as an axiomatic type class as follows. Note that the wenzelm@37671 16 parent class $\idt{times}$ is provided by the basic HOL theory. *} wenzelm@6763 17 haftmann@35317 18 class group = times + one + inverse + wenzelm@37671 19 assumes group_assoc: "(x * y) * z = x * (y * z)" wenzelm@37671 20 and group_left_one: "1 * x = x" wenzelm@37671 21 and group_left_inverse: "inverse x * x = 1" wenzelm@6763 22 wenzelm@37671 23 text {* The group axioms only state the properties of left one and wenzelm@37671 24 inverse, the right versions may be derived as follows. *} wenzelm@6763 25 wenzelm@37671 26 theorem (in group) group_right_inverse: "x * inverse x = 1" wenzelm@10007 27 proof - wenzelm@37671 28 have "x * inverse x = 1 * (x * inverse x)" wenzelm@10141 29 by (simp only: group_left_one) wenzelm@37671 30 also have "... = 1 * x * inverse x" wenzelm@10007 31 by (simp only: group_assoc) wenzelm@10141 32 also have "... = inverse (inverse x) * inverse x * x * inverse x" wenzelm@10007 33 by (simp only: group_left_inverse) wenzelm@10141 34 also have "... = inverse (inverse x) * (inverse x * x) * inverse x" wenzelm@10007 35 by (simp only: group_assoc) wenzelm@37671 36 also have "... = inverse (inverse x) * 1 * inverse x" wenzelm@10007 37 by (simp only: group_left_inverse) wenzelm@37671 38 also have "... = inverse (inverse x) * (1 * inverse x)" wenzelm@10007 39 by (simp only: group_assoc) wenzelm@10141 40 also have "... = inverse (inverse x) * inverse x" wenzelm@10141 41 by (simp only: group_left_one) wenzelm@37671 42 also have "... = 1" wenzelm@10007 43 by (simp only: group_left_inverse) wenzelm@10007 44 finally show ?thesis . wenzelm@10007 45 qed wenzelm@6763 46 wenzelm@37671 47 text {* With \name{group-right-inverse} already available, wenzelm@37671 48 \name{group-right-one}\label{thm:group-right-one} is now established wenzelm@37671 49 much easier. *} wenzelm@6763 50 wenzelm@37671 51 theorem (in group) group_right_one: "x * 1 = x" wenzelm@10007 52 proof - wenzelm@37671 53 have "x * 1 = x * (inverse x * x)" wenzelm@10007 54 by (simp only: group_left_inverse) wenzelm@10141 55 also have "... = x * inverse x * x" wenzelm@10007 56 by (simp only: group_assoc) wenzelm@37671 57 also have "... = 1 * x" wenzelm@10007 58 by (simp only: group_right_inverse) wenzelm@10007 59 also have "... = x" wenzelm@10141 60 by (simp only: group_left_one) wenzelm@10007 61 finally show ?thesis . wenzelm@10007 62 qed wenzelm@6763 63 wenzelm@37671 64 text {* \medskip The calculational proof style above follows typical wenzelm@37671 65 presentations given in any introductory course on algebra. The wenzelm@37671 66 basic technique is to form a transitive chain of equations, which in wenzelm@37671 67 turn are established by simplifying with appropriate rules. The wenzelm@37671 68 low-level logical details of equational reasoning are left implicit. wenzelm@6784 69 wenzelm@37671 70 Note that $\dots$'' is just a special term variable that is bound wenzelm@37671 71 automatically to the argument\footnote{The argument of a curried wenzelm@37671 72 infix expression happens to be its right-hand side.} of the last wenzelm@37671 73 fact achieved by any local assumption or proven statement. In wenzelm@37671 74 contrast to $\var{thesis}$, the $\dots$'' variable is bound wenzelm@37671 75 \emph{after} the proof is finished, though. wenzelm@7874 76 wenzelm@37671 77 There are only two separate Isar language elements for calculational wenzelm@37671 78 proofs: \isakeyword{also}'' for initial or intermediate wenzelm@37671 79 calculational steps, and \isakeyword{finally}'' for exhibiting the wenzelm@37671 80 result of a calculation. These constructs are not hardwired into wenzelm@37671 81 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. wenzelm@37671 82 Expanding the \isakeyword{also} and \isakeyword{finally} derived wenzelm@37671 83 language elements, calculations may be simulated by hand as wenzelm@37671 84 demonstrated below. wenzelm@10007 85 *} wenzelm@6784 86 wenzelm@37671 87 theorem (in group) "x * 1 = x" wenzelm@10007 88 proof - wenzelm@37671 89 have "x * 1 = x * (inverse x * x)" wenzelm@10007 90 by (simp only: group_left_inverse) wenzelm@6763 91 wenzelm@7433 92 note calculation = this wenzelm@10007 93 -- {* first calculational step: init calculation register *} wenzelm@6763 94 wenzelm@10141 95 have "... = x * inverse x * x" wenzelm@10007 96 by (simp only: group_assoc) wenzelm@6763 97 wenzelm@7433 98 note calculation = trans [OF calculation this] wenzelm@10007 99 -- {* general calculational step: compose with transitivity rule *} wenzelm@6763 100 wenzelm@37671 101 have "... = 1 * x" wenzelm@10007 102 by (simp only: group_right_inverse) wenzelm@6763 103 wenzelm@7433 104 note calculation = trans [OF calculation this] wenzelm@10007 105 -- {* general calculational step: compose with transitivity rule *} wenzelm@6763 106 wenzelm@10007 107 have "... = x" wenzelm@10141 108 by (simp only: group_left_one) wenzelm@6763 109 wenzelm@7433 110 note calculation = trans [OF calculation this] wenzelm@10007 111 -- {* final calculational step: compose with transitivity rule ... *} wenzelm@6784 112 from calculation wenzelm@10007 113 -- {* ... and pick up the final result *} wenzelm@6763 114 wenzelm@10007 115 show ?thesis . wenzelm@10007 116 qed wenzelm@6763 117 wenzelm@37671 118 text {* Note that this scheme of calculations is not restricted to wenzelm@37671 119 plain transitivity. Rules like anti-symmetry, or even forward and wenzelm@37671 120 backward substitution work as well. For the actual implementation wenzelm@37671 121 of \isacommand{also} and \isacommand{finally}, Isabelle/Isar wenzelm@37671 122 maintains separate context information of transitivity'' rules. wenzelm@37671 123 Rule selection takes place automatically by higher-order wenzelm@37671 124 unification. *} wenzelm@7874 125 wenzelm@6763 126 wenzelm@10007 127 subsection {* Groups as monoids *} wenzelm@6793 128 wenzelm@37671 129 text {* Monoids over signature $({\times} :: \alpha \To \alpha \To wenzelm@37671 130 \alpha, \idt{one} :: \alpha)$ are defined like this. wenzelm@10007 131 *} wenzelm@6793 132 haftmann@35317 133 class monoid = times + one + wenzelm@37671 134 assumes monoid_assoc: "(x * y) * z = x * (y * z)" wenzelm@37671 135 and monoid_left_one: "1 * x = x" wenzelm@37671 136 and monoid_right_one: "x * 1 = x" wenzelm@6793 137 wenzelm@37671 138 text {* Groups are \emph{not} yet monoids directly from the wenzelm@37671 139 definition. For monoids, \name{right-one} had to be included as an wenzelm@37671 140 axiom, but for groups both \name{right-one} and \name{right-inverse} wenzelm@37671 141 are derivable from the other axioms. With \name{group-right-one} wenzelm@37671 142 derived as a theorem of group theory (see wenzelm@37671 143 page~\pageref{thm:group-right-one}), we may still instantiate wenzelm@37671 144 $\idt{group} \subseteq \idt{monoid}$ properly as follows. *} wenzelm@6793 145 wenzelm@10007 146 instance group < monoid wenzelm@37671 147 by intro_classes wenzelm@37671 148 (rule group_assoc, wenzelm@37671 149 rule group_left_one, wenzelm@37671 150 rule group_right_one) wenzelm@6793 151 wenzelm@37671 152 text {* The \isacommand{instance} command actually is a version of wenzelm@37671 153 \isacommand{theorem}, setting up a goal that reflects the intended wenzelm@37671 154 class relation (or type constructor arity). Thus any Isar proof wenzelm@37671 155 language element may be involved to establish this statement. When wenzelm@37671 156 concluding the proof, the result is transformed into the intended wenzelm@37671 157 type signature extension behind the scenes. *} wenzelm@37671 158 wenzelm@7874 159 wenzelm@10141 160 subsection {* More theorems of group theory *} wenzelm@10141 161 wenzelm@37671 162 text {* The one element is already uniquely determined by preserving wenzelm@37671 163 an \emph{arbitrary} group element. *} wenzelm@10141 164 wenzelm@37671 165 theorem (in group) group_one_equality: wenzelm@37671 166 assumes eq: "e * x = x" wenzelm@37671 167 shows "1 = e" wenzelm@10141 168 proof - wenzelm@37671 169 have "1 = x * inverse x" wenzelm@10141 170 by (simp only: group_right_inverse) wenzelm@10141 171 also have "... = (e * x) * inverse x" wenzelm@10141 172 by (simp only: eq) wenzelm@10141 173 also have "... = e * (x * inverse x)" wenzelm@10141 174 by (simp only: group_assoc) wenzelm@37671 175 also have "... = e * 1" wenzelm@10141 176 by (simp only: group_right_inverse) wenzelm@10141 177 also have "... = e" wenzelm@10141 178 by (simp only: group_right_one) wenzelm@10141 179 finally show ?thesis . wenzelm@10141 180 qed wenzelm@10141 181 wenzelm@37671 182 text {* Likewise, the inverse is already determined by the cancel property. *} wenzelm@10141 183 wenzelm@37671 184 theorem (in group) group_inverse_equality: wenzelm@37671 185 assumes eq: "x' * x = 1" wenzelm@37671 186 shows "inverse x = x'" wenzelm@10141 187 proof - wenzelm@37671 188 have "inverse x = 1 * inverse x" wenzelm@10141 189 by (simp only: group_left_one) wenzelm@10141 190 also have "... = (x' * x) * inverse x" wenzelm@10141 191 by (simp only: eq) wenzelm@10141 192 also have "... = x' * (x * inverse x)" wenzelm@10141 193 by (simp only: group_assoc) wenzelm@37671 194 also have "... = x' * 1" wenzelm@10141 195 by (simp only: group_right_inverse) wenzelm@10141 196 also have "... = x'" wenzelm@10141 197 by (simp only: group_right_one) wenzelm@10141 198 finally show ?thesis . wenzelm@10141 199 qed wenzelm@10141 200 wenzelm@37671 201 text {* The inverse operation has some further characteristic properties. *} wenzelm@10141 202 wenzelm@37671 203 theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x" wenzelm@10141 204 proof (rule group_inverse_equality) wenzelm@37671 205 show "(inverse y * inverse x) * (x * y) = 1" wenzelm@10141 206 proof - wenzelm@10141 207 have "(inverse y * inverse x) * (x * y) = wenzelm@10141 208 (inverse y * (inverse x * x)) * y" wenzelm@10141 209 by (simp only: group_assoc) wenzelm@37671 210 also have "... = (inverse y * 1) * y" wenzelm@10141 211 by (simp only: group_left_inverse) wenzelm@10141 212 also have "... = inverse y * y" wenzelm@10141 213 by (simp only: group_right_one) wenzelm@37671 214 also have "... = 1" wenzelm@10141 215 by (simp only: group_left_inverse) wenzelm@10141 216 finally show ?thesis . wenzelm@10141 217 qed wenzelm@10141 218 qed wenzelm@10141 219 wenzelm@37671 220 theorem (in group) inverse_inverse: "inverse (inverse x) = x" wenzelm@10141 221 proof (rule group_inverse_equality) wenzelm@10141 222 show "x * inverse x = one" wenzelm@10141 223 by (simp only: group_right_inverse) wenzelm@10141 224 qed wenzelm@10141 225 wenzelm@37671 226 theorem (in group) inverse_inject: wenzelm@37671 227 assumes eq: "inverse x = inverse y" wenzelm@37671 228 shows "x = y" wenzelm@10141 229 proof - wenzelm@37671 230 have "x = x * 1" wenzelm@10141 231 by (simp only: group_right_one) wenzelm@10141 232 also have "... = x * (inverse y * y)" wenzelm@10141 233 by (simp only: group_left_inverse) wenzelm@10141 234 also have "... = x * (inverse x * y)" wenzelm@10141 235 by (simp only: eq) wenzelm@10141 236 also have "... = (x * inverse x) * y" wenzelm@10141 237 by (simp only: group_assoc) wenzelm@37671 238 also have "... = 1 * y" wenzelm@10141 239 by (simp only: group_right_inverse) wenzelm@10141 240 also have "... = y" wenzelm@10141 241 by (simp only: group_left_one) wenzelm@10141 242 finally show ?thesis . wenzelm@10141 243 qed wenzelm@10141 244 wenzelm@10141 245 end