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